[TYPES] mechanized formalizations of the pi calculus

Wed Apr 8 07:32:17 EDT 2015

Dear types-list,

I'm trying to construct a complete bibliography of formalizations/proofs of
properties of the pi calculus, or close relatives (typed, untyped, applied,
...), in any system.  The references I've found so far (from a morning of
Googling) are at the end of this message.

I have the impression that there are probably formalizations out there that
have been performed in other contexts (e.g. in modeling security
protocols), and it might not be easy to find these examples from searching
paper titles/abstracts.  Also, there may be tutorial or demo examples that
haven't been described by publications.  So, I'd welcome any suggestions
I've missed - either of formalizations themselves, or publications
describing them.

I'm also interested in understanding which approaches are suitable / have
been successful for proving different properties, and in the track records
of different approaches with respect to extensibility or reuse.

I'm happy to collect responses off-list and summarize to the list.

--James

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, UK, 1-16.

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, 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, UK, 425-439.

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.

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, UK,
217-232.

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

Christine Röckl and Daniel Hirschkoff. 2003. A fully adequate shallow
embedding of the π-calculus in Isabelle F;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

Murdoch J. Gabbay,

*in “Thirty Five Years of Automating Mathematics”, Kluwer Applied Logic
series, Volume 28, Pages 247-269, 2004, ISBN 978-1-4020-1656-5*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

Jesper Bengtson and Joachim Parrow. 2007. Formalising the \&\#960;-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

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

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

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
<http://dblp.uni-trier.de/pers/hd/p/Parrow:Joachim>:
Formalising the pi-calculus using nominal logic. Logical Methods in
Computer Science 5(2)
<http://dblp.uni-trier.de/db/journals/lmcs/lmcs5.html#abs-0809-3960> (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

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

Jesper Bengtson, Magnus Johansson
<http://dblp.uni-trier.de/pers/hd/j/Johansson:Magnus>, Joachim Parrow
<http://dblp.uni-trier.de/pers/hd/p/Parrow:Joachim>, Björn Victor
<http://dblp.uni-trier.de/pers/hd/v/Victor:Bj=ouml=rn>:
Psi-calculi: a framework for mobile processes with nominal data and
logic. Logical
Methods in Computer Science 7(1)
<http://dblp.uni-trier.de/db/journals/lmcs/lmcs7.html#abs-1101-3262> (2011)

Jesper Bengtson:
The pi-calculus in nominal logic. Archive of Formal Proofs 2012
<http://dblp.uni-trier.de/db/journals/afp/afp2012.html#Bengtson12a> (2012)

Jesper Bengtson:
Psi-calculi in Isabelle. Archive of Formal Proofs 2012
<http://dblp.uni-trier.de/db/journals/afp/afp2012.html#Bengtson12> (2012)