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.


Published in:
Proc. MERLIN'01
Presented at:
MERLIN'01, June 2001
Year:
2001
Laboratories:




 Record created 2006-01-24, last modified 2018-03-17

n/a:
Download fulltext
PS.GZ

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)