Psi-calculi in Isabelle

Jesper Bengtson, Joachim Parrow, Tjark Weber

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

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.
Original languageEnglish
Article number1
JournalJournal of Automated Reasoning
Volume56
Issue number1
Pages (from-to)1-47
Number of pages1
ISSN0168-7433
DOIs
Publication statusPublished - 13 Jan 2016

Keywords

  • Process calculi
  • Interactive proof assistants
  • Isabelle

Fingerprint

Dive into the research topics of 'Psi-calculi in Isabelle'. Together they form a unique fingerprint.

Cite this