Jesper Bengtson, Joachim Parrow, and Tjark Weber. Journal of Automated Reasoning, 56(1):1-47, 2016.
This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. Psi-calculi are significantly more expressive, yet their semantics is as simple in structure as the semantics of the original pi-calculus. Proofs of meta-theoretic properties for psi-calculi are more involved, however, not least because psi-calculi (unlike simpler calculi) utilise binders that bind multiple names at once. The mechanisation is carried out in the Nominal Isabelle framework, an interactive proof assistant designed to facilitate formal reasoning about calculi with binders. Our main contributions are twofold. First, we have developed techniques that allow efficient reasoning about calculi that bind multiple names in Nominal Isabelle. Second, we have adopted these techniques to mechanise substantial results from the meta-theory of psi-calculi, including congruence properties of bisimilarity and the laws of structural congruence. To our knowledge, this is the most extensive formalisation of process calculi mechanised in a proof assistant to date.
The original publication is available at www.springerlink.com.
@article{bengtson16psi,
author = {Jesper Bengtson and Joachim Parrow and Tjark Weber},
title = {Psi-Calculi in {Isabelle}},
journal = {Journal of Automated Reasoning},
volume = {56},
number = {1},
pages = {1--47},
year = {2016},
url = {http://dx.doi.org/10.1007/s10817-015-9336-2},
doi = {10.1007/s10817-015-9336-2},
}