Interactive Theorem Provers

Motivation

Using interactive theorem provers to do mathematical proofs has long been a goal of many mathematicians and computer scientists. The prospect of having proofs fully machine checked is appealing, but the tools available have been cumbersome to work with since computers lack the intuitive grasp of mathematics that we humans possess. A statement such as: by induction over P we clearly see that... might be fully acceptable in a paper proof but a theorem prover will not allow it since to such a program, nothing is intuitively clear.

The main motivation for our work is to make theorems for the pi-calculus within a theorem prover which resembles their pen-and-paper equivalents to as high a degree as possible especially when it comes to abstraction of alpha-equivalent terms.

Results

We have used the theorem prover Isabelle to formalise a substantial part of the pi-calculus. At the core of our formalisation lies the nominal datatype package developed by Christian Urban and Stefan Berghofer. The nominal datatype package is based on the theories of Nominal Logic by Andrew Pitts et. al.

Our formalisation is, to our knowledge, the most extensive formalisation of a mobile calculus ever to be done inside a theorem prover. It includes the following:

• Formalisations of both late and early semantics of the monadic pi-calculus, with proofs that:
  • Strong bisimulation is an equivalence relation and preserved by all operators except the input prefix.
  • Strong equivalence is a congruence.
  • Weak bisimulation is preserved by all operators except sum and input prefix.
  • Weak congruence is a congruence
  • Proofs that all early bisimulation relations are included in their late counterparts.
• A set of algebraic laws, including the tau-laws and the Hennessy lemma.
• A proof that the axiomatization of strong late bisimilarity is sound and complete.

The completeness proof is the first of its kind to be completely machine checked.

The image on the right contains a sample proof from our formalisation.

The source code for our formalisation can be found here.

Ongoing work

We are currently working with Microsoft Research in Cambridge in their project Samoa to integrate our ideas in a set of tools for securing web services.

Related work

Theorem provers have been used before to model process algebras. When modelling a process algebra one must deal with its binders in some way. The two most command ways have to date been de-Bruijn indices and higher order abstract syntax (HOAS). Early work by Daniel Hirschkoff modelled the pi-calculus in Coq using de-Bruijn indices. Christine Röckl modelled the pi-calculus in Isabelle using HOAS and Furio Honsel et. al. did the same using Coq.

Publications