Tuesday, April 14, 2015

Mechanized formalizations of the pi-calculus (and friends)

I recently started to put together a bibliography (as complete as I can make it) of mechanized formalizations of the pi-calculus (and close relations).  I also asked for additional suggestions on the TYPES mailing list, and received several helpful responses.  Here is the complete list, as of today.

I hope to use this as a starting point to understand the strengths and weaknesses of different approaches (and any gaps in the literature) but so far I have not read most of these papers.  Nevertheless I am posting this without any further discussion in case it is helpful to anyone else interested in this topic in the future.

Thanks to Robert Harper, Dale Miller, Dominic Orchard, Francois Pottier, Ivan Scagnetto, Gabriel Scherer, and Tjark Weber for their suggestions.

[Updated: Thanks also to Tobias Nipkow and Jeremy Siek for spotting some typos and misclassifications, and Alan Schmitt for a link to more information on HOCore.]

[Updated 2: to include Christine Rockl's MERLIN 2001 paper on a formalization of the pi-calculus in Isabelle/HOL using Gabbay-Pitts permutation-based syntax.]

[Updated 3: to include more recent work on formalising psi-calculi using Nominal Isabelle.]
Read more »

Labels: ,