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.]

Agda

Coq

  • Daniel Hirschkoff. 1997. A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions. In Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '97), Elsa L. Gunter and Amy P. Felty (Eds.). Springer-Verlag, London, UK, 153-169.
  • Joëlle Despeyroux. 2000. A Higher-Order Specification of the pi-Calculus. In Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics (TCS '00), Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito (Eds.). Springer-Verlag, London, UK, 425-439.
  • Furio Honsell, Marino Miculan, and Ivan Scagnetto. 2001. Pi-calculus in (Co)inductive-type theory. Theor. Comput. Sci. 253, 2 (February 2001), 239-285. DOI=10.1016/S0304-3975(00)00095-5 http://dx.doi.org/10.1016/S0304-3975(00)00095-5
  • Ivan Scagnetto, Marino Miculan. Ambient Calculus and its Logic in the Calculus of Inductive Constructions. In Proceedings of LFM 2002. ENTCS 70.2, Elsevier, 2002.(http://www.sciencedirect.com/science/article/pii/S1571066104805073)
  • Reynald Affeldt and Naoki Kobayashi. 2008. A Coq Library for Verification of Concurrent Programs. Electron. Notes Theor. Comput. Sci. 199 (February 2008), 17-32. DOI=10.1016/j.entcs.2007.11.010 http://dx.doi.org/10.1016/j.entcs.2007.11.010
  • "HOCore in Coq", Martín Escarrá, Maksimović Petar, Alan Schmitt https://hal.inria.fr/hal-01099130 and see also this web page with an updated paper and formalization: https://www.irisa.fr/celtique/aschmitt/research/hocore/

HOL

  • T. F. Melham. 1994. A mechanized theory of the pi-calculus in HOL. Nordic J. of Computing 1, 1 (March 1994), 50-76.
  • Otmane Aït Mohamed. 1995. Mechanizing a pi-Calculus Equivalence in HOL. In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, E. Thomas Schubert, Phillip J. Windley, and Jim Alves-Foss (Eds.). Springer-Verlag, London, UK, 1-16.

Isabelle/HOL

  • Simon J. Gay. 2001. A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. In Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '01), Richard J. Boulton and Paul B. Jackson (Eds.). Springer-Verlag, London, UK, 217-232. 
  • A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations. Electr. Notes Theor. Comput. Sci. 58(1): 1-17 ()
  • Christine Röckl, Daniel Hirschkoff, and Stefan Berghofer. 2001. Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts. In Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS '01), Furio Honsell and Marino Miculan (Eds.). Springer-Verlag, London, UK, UK, 364-378. 
  • Christine Röckl and Daniel Hirschkoff. 2003. A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis. J. Funct. Program. 13, 2 (March 2003), 415-451. DOI=10.1017/S0956796802004653 http://dx.doi.org/10.1017/S0956796802004653

Isabelle/HOL-Nominal

Lambda-Prolog/Lambda-term abstract syntax/Abella

(Concurrent) LF

  • Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2008. Specifying Properties of Concurrent Computations in CLF. Electron. Notes Theor. Comput. Sci. 199 (February 2008), 67-87. DOI=10.1016/j.entcs.2007.11.013 http://dx.doi.org/10.1016/j.entcs.2007.11.013

Labels: ,

4 Comments:

At April 14, 2015 9:06 pm , Anonymous Anonymous said...

Some doi are missing (for instance, http://dx.doi.org/10.1007/3-540-45315-6_24 ), you should use http://www.crossref.org/guestquery/ or http://www.informatik.uni-trier.de/~ley/db/ to get them all.

 
At April 14, 2015 10:53 pm , Blogger James Cheney said...

Thanks. I was just trying to build a bibliography quickly and copied from various sources (some of which don't include DOIs) without trying to make everything perfect, but it would be good to add links and DOIs. I'll do that as time permits.

 
At April 15, 2015 5:37 pm , Blogger Jeremy Siek said...

Thanks for this post!

"additional syggesgions"
->
"additional suggestions"

 
At April 15, 2015 5:53 pm , Blogger James Cheney said...

Do'h! Fixed, thanks.

 

Post a Comment

Subscribe to Post Comments [Atom]

Links to this post:

Create a Link

<< Home