A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations

A formalized theory of alpha-conversion for the pi-calculus in Isabelle/HOL is presented. Following a recent proposal by Gabbay and Pitts, substitutions are modelled in terms of permutations, and alpha-equivalence is defined over all but finitely many names. In contrast to the work by Gabbay and Pitts, however, standard universal and existential quantification are used instead of introducing a new binder. Further, a classification of the various approaches to formalizing languages with binders is presented. Strengths and weaknesses are pointed out, and suggestions for possible applications are made.