Interactive Theorem Proving

Proving a mathematical theorem may require creativity, a deep understanding of the subject matter and sometimes a stroke of genius. It is such a challenging endeavor that even the greatest mathematicians are not immune to making mistakes.

On the other hand, checking the correctness of a given proof should require neither creativity nor ingenuity. It should be a straightforward exercise that simply comprises validating each argument made in the proof, line by line. In practice, however, traditional mathematical proofs can still be exceedingly hard to check.

Interactive theorem proving makes the dream of easy-to-check proofs a reality. An interactive theorem prover is a software tool that facilitates the development of formal proofs through human-computer collaboration. The human user provides conjectures and guides the machine towards a proof; the software keeps track of details and fills in some trivial steps. Checking proofs written in an interactive theorem prover becomes so simple that it can, in fact, be done fully automatically.

Consequently, any element of human error is eliminated. The machine-checked theorems that are obtained via interactive theorem proving are extremely trustworthy.

We use interactive theorem proving to reason about concurrent systems and models of concurrency. We are especially interested in the theory of process calculi, including theorems about the pi-calculus and related calculi.

A particular challenge in this area is the formalization of name binding. In informal proofs, alpha-equivalent terms, e.g., a(x). P[x] and a(y). P[y], are typically considered equal. In formal proofs however, where no appeal to human intuition is possible, every reasoning step has to be precisely justified. We aim to obtain formal proofs that resemble their informal counterparts as closely as possible.

To this end we are using the interactive theorem prover Isabelle and its nominal datatype package. The latter is based on Nominal Logic, a theory of names and binding by Andrew Pitts et al.

We have formalized a substantial part of the theory of the pi-calculus and of Psi calculi in Isabelle.

To our knowledge, this is the most extensive formalization of mobile calculi ever carried out in a theorem prover. It includes the following:

• Formalizations 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 was the first of its kind to be completely machine checked.

The image below contains a sample proof from our formalization.

Our formalizations of the pi-calculus and of Psi calculi are available from the Archive of Formal Proofs.

We have also worked with Microsoft Research (Cambridge) on the Samoa project to integrate our ideas in a set of tools for securing web services.