Some π-calculus meta-theory

The π-calculus provides an appealing example of using Abella in meta-theory reasoning. The following paper describe in detail how the π-calculus and some of its meta-theory can be encoded in a logic using fixed points and the ∇-quantifier.

[TM09] Proof Search Specifications of Bisimulation and Modal Logics for the π-calculus, by Alwen Tiu and Dale Miller. Accepted (February 2009) to the ACM Transactions on Computational Logic. Draft dated 16 February 2009: (pdf, arXiv)

Some of the examples in these papers can be directly represented in Abella. In particular, Figures 2 and 5 in [TM09] contain a specification of the π-calculus containing the bang operators. That specification can be found in the two λProlog files pic.sig and pic.mod. In Example 28 of [TM09], two π-calculus expressions are claimed to be bisimilar. A complete proof of this bisimulation is given in the Abella theorem file pic.thm (HTML version). This theorem file also includes proofs that bisimulation is reflexive and symmetric.

The following specification and results focus on the "finite π-calculus": that is, the π-calculus without the "bang" (!) constructor and without recursive definitions. This sub-calculus is useful for focusing on the treatment of bindings when dealing with the π-calculus.

  1. The files finite-pic.sig and finite-pic.mod are λProlog specification files.
  2. The finite-pic.thm (HTML version) contains an Abella theory file that defines simulation and bisimulation coinductively and then proves that simulation is preorder and bisimulation is an equivalence relation.
  3. The finite-pic-cong.thm (HTML version) contains an Abella theory file that proves that simulation is a pre-congruence. Following the proof in that file, it should be straightforward to show that bisimulation is a congruence. Notice that the bisimulation defined using the intuitionistic theory in Abella corresponds to open bisimulation (see D. Sangiorgi, ``A Theory of Bisimulation for the π-Calculus'', Acta Informatica 33(1), pp. 69-97, 1996).

In all cases, the proofs of the theorems are rather natural and high-level although they are completely formal. All issues involving bindings, names, and substitutions are handled declaratively without explicit side-conditions.