Département d'Informatique
Laboratoire des Méthodes de Programmation
(LAMP)
Ecole Politechnique Federale de Lausanne

 

The Pi-Calculus in Isabelle/HOL

This page is about work I did for my PhD thesis and shortly afterwards. The objective was to find a foundation for formalizing languages such as the pi-calculus in general-purpose theorem-provers so to be able to conduct proofs about concrete systems. To keep things as simple as possible I have focussed on a monadic pi-calculus, although it might be challenging to see how things work out for a polyadic version. I do have some ideas in mind, but I cannot promise I will find the time to elaborate them in the near future.

In general, there exist three ways to formalize languages with binders in an interactive theorem-prover like Isabelle using its (most current, I would say) object-logic HOL:
  • First-order syntax in a deep embedding: The "classical" approach, one could say. The problem is that one has to define and use explicitely some notion of substitution in order to account for alpha-conversion and instantiations. This can be quite cumbersome. Another inconvenience is that in descriptions of concrete systems in thy-files one has to define a constant for each bound name, which is a bit of a hack.
  • Higher-order syntax in a deep embedding: Nice theoretical variant, because one can delegate alpha-conversion and instantiations to an underlying lambda-calculus for which substitutions can be defined much more easily (often, formalizations of the lambda-calculus already exist and can be taken as a basis). However, there is still quite a bit of interaction, and still one has to use pre-defined constants for bound names in thy-files.
  • Higher-order syntax in a shallow embedding: Give your formalization the meta-level boost! Everything that has to do with bound names is delegated to the meta-level of the theorem-prover. Therefore, one does not have to care about alpha-conversion any longer, and instantiations are mere function applications. Of course, this approach has its drawbacks as well (loss of structural induction, sometimes exotic terms). Luckily, something can be done about this...
I have given the first and third alternative a try. Below, you can find the respective sources, in addition with papers written about the attempts. I have also given a full abstraction proof for the higher-order approach with respect to a straightforward first-order syntax (using an older version of Isabelle, sorry!), please consult my old web-page for that.

Back to my homepage.

 

 The Pi-Calculus in First-Order Syntax

The formalization is based on two ideas proposed by Gabbay and Pitts: use permutations instead of substitutions to obtain a symmetric operation, and reason about all but finitely many instantiations. However, in contrast to their proposal, I do not introduce a new quantifier for that but use standard universal and existential quantification.

 

 The Pi-Calculus in Higher-Order Abstract Syntax

Using the functional mechanisms provided by Isabelle's meta-level, one does not have to bother about bound names any more. Exotic terms are ruled out, and induction is obtained, by using inductive well-formedness predicates adapting ideas expressed by Despeyroux, Felty, and Hirschowitz. The semantics is based on abstractions and concretions which naturally fit into a higher-order approach.