|
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.
|
