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 »

Two reversible forms of CCS

Danos, V. and Krivine, J., Reversible communicating systems. CONCUR 2004, LNCS, 3170. pp. 292-307.

Iain C. C. Phillips, Irek Ulidowski: Reversing algebraic process calculi. J. Log. Algebr. Program. 73(1-2): 70-96 (2007)

These two papers present different views on reversibility for CCS.  In both cases, a key question is how to deal with a process term such as $(a.P | a.Q | \bar{a}.R| \bar{a}.S) \backslash a$ which can evolve in two different ways, both leading to the same state $(P|Q|R|S)$: one where the $a.P$ and $\bar{a}.R$ synchronize, and one where $a.P$ and $\bar{a}.S$ synchronize.  A key question is, what additional information do we need to record so that the right synchronizations are undone.

Read more »

A model for distributed systems based on graph rewriting

A model for distributed systems based on graph rewriting
P. Degano and U. Montanari
J ACM 34(2):411-449

I was pointed to this paper by Eric Griffis, a student who will be visiting this summer as part of a NSF PIRE program.  Eric is interested in graph rewriting and distributed systems.

The paper presents a generic computational model for concurrent/distributed computation based on graphs (really, hypergraphs).  The "nodes" of the hypergraphs correspond to channels, and the "hyperedges" correspond to either events (interactions in the past) or processes (placeholders for possible interactions in the future).  Thus, the graph as a whole describes both the past (previous events), present (frontier of active processes that can make progress now) and future (processes whose progress is blocked by other processes).

The execution behavior of the system can be specified using graph rewriting.  Production rules are specified as mappings from nonterminal labels to graph fragments.  Rewrite rules are obtained from these by merging concurrent events.  The meaning of a system (that possibly runs forever) is defined by setting up a ultrametric space on graph states and taking limits.  (This is a large oversimplification.)
Read more »