The PiCalculus 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 picalculus in generalpurpose theoremprovers so to be able
to conduct proofs about concrete systems. To keep things as
simple as possible I have focussed on a monadic picalculus, 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 theoremprover like
Isabelle
using its (most current, I would say) objectlogic
HOL:
 Firstorder 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 alphaconversion and
instantiations. This can be quite cumbersome. Another
inconvenience is that in descriptions of concrete systems
in thyfiles one has to define a constant for each bound
name, which is a bit of a hack.
 Higherorder syntax in a deep embedding:
Nice theoretical variant, because one can delegate
alphaconversion and instantiations to an underlying
lambdacalculus for which substitutions can be defined
much more easily (often, formalizations of the lambdacalculus
already exist and can be taken as a basis). However, there
is still quite a bit of interaction, and still one has
to use predefined constants for bound names in thyfiles.
 Higherorder syntax in a shallow embedding:
Give your formalization the metalevel boost! Everything
that has to do with bound names is delegated to the
metalevel of the theoremprover. Therefore, one does
not have to care about alphaconversion 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 higherorder approach with
respect to a straightforward firstorder syntax (using
an older version of Isabelle, sorry!), please consult my
old
webpage for that.
Back to my homepage.
