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

• Dominic Orchard, Nobuko Yoshida, "Using session types as an effect system", PLACES 2015, http://www.doc.ic.ac.uk/~dorchard/publ/effects-as-sessions-places15.pdf, with formalization of a translation from effects to sessions types:  https://github.com/dorchard/effects-as-sessions/

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. 
• Christine Röckl.  A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations. Electr. Notes Theor. Comput. Sci. 58(1): 1-17 (2001)
• 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

• Murdoch J. Gabbay, The pi-calculus in FM, in “Thirty Five Years of Automating Mathematics”, Kluwer Applied Logic series, Volume 28, Pages 247-269, 2004, ISBN 978-1-4020-1656-5.  (This doesn't describe a full formalization but uses nominal-style representation in Fraenkel-Mostowski set theory.)
• Jesper Bengtson and Joachim Parrow. 2007. Formalising the pi-calculus using nominal logic. In Proceedings of the 10th international conference on Foundations of software science and computational structures (FOSSACS'07), Helmut Seidl (Ed.). Springer-Verlag, Berlin, Heidelberg, 63-77.
• Jesper Bengtson and Joachim Parrow. 2007. A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle. Electron. Notes Theor. Comput. Sci. 192, 1 (October 2007), 61-75. DOI=10.1016/j.entcs.2007.08.017 http://dx.doi.org/10.1016/j.entcs.2007.08.017
• Temesghen Kahsai and Marino Miculan. 2008. Implementing Spi Calculus Using Nominal Techniques. In Proceedings of the 4th conference on Computability in Europe: Logic and Theory of Algorithms (CiE '08), Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Lowe (Eds.). Springer-Verlag, Berlin, Heidelberg, 294-305. DOI=10.1007/978-3-540-69407-6_33 http://dx.doi.org/10.1007/978-3-540-69407-6_33
• Jesper Bengtson, Joachim Parrow: Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science 5(2) (2009)
• Jesper Bengtson and Joachim Parrow. 2009. Psi-calculi in Isabelle. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer-Verlag, Berlin, Heidelberg, 99-114. DOI=10.1007/978-3-642-03359-9_9 http://dx.doi.org/10.1007/978-3-642-03359-9_9
• Jesper Bengtson, Magnus Johansson, Joachim Parrow, Björn Victor: Psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods in Computer Science 7(1) (2011)
• Jesper Bengtson: The pi-calculus in nominal logic. Archive of Formal Proofs 2012 (2012)
• Jesper Bengtson: Psi-calculi in Isabelle. Archive of Formal Proofs 2012 (2012) (apparently there is a Journal of Automated Reasoning article on this in press, with Joachim Parrow and Tjark Weber.)
• Johannes Borgström, Ramunas Gutkovas, Joachim Parrow, Björn Victor, Johannes Åman Pohjola: A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract). TGC 2013: 103-118
• Joachim Parrow, Johannes Borgström, Palle Raabjerg, Johannes Åman Pohjola:
  Higher-order psi-calculi. Mathematical Structures in Computer Science 24(2) (2014)
• Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, Joachim Parrow: Broadcast psi-calculi with an application to wireless protocols. Software and System Modeling 14(1): 201-216 (2015)

Lambda-Prolog/Lambda-term abstract syntax/Abella

• Alwen Tiu and Dale Miller. 2005. A Proof Search Specification of the π-Calculus. Electron. Notes Theor. Comput. Sci. 138, 1 (September 2005), 79-101. DOI=10.1016/j.entcs.2005.05.006 http://dx.doi.org/10.1016/j.entcs.2005.05.006
• Alwen Tiu and Dale Miller. 2010. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. Comput. Logic 11, 2, Article 13 (January 2010), 35 pages. DOI=10.1145/1656242.1656248 http://doi.acm.org/10.1145/1656242.1656248 
• David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang: Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7(2):1-89, 2014 (a tutorial that devotes several pages to the pi-calculus; see also http://abella-prover.org/examples/process-calculi/pi-calculus/ and http://abella-prover.org/upto/)
• Tiu, Alwen, and Jeremy Dawson. "Automating open bisimulation checking for the spi calculus." IEEE Computer Security Foundations Symposium (CSF), 2010 . IEEE, 2010.

(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