Publication
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.
Carmela González Troncoso, Giovanni Cherubin
David Lyndon Emsley, Pierrick Berruyer, Andrea Bertarello