Psi-calculi in Isabelle

Jesper Bengtson, Joachim Parrow, Tjark Weber

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
Artikelnummer1
TidsskriftJournal of Automated Reasoning
Vol/bind56
Udgave nummer1
Sider (fra-til)1-47
Antal sider1
ISSN0168-7433
DOI
StatusUdgivet - 13 jan. 2016

Fingeraftryk

Dyk ned i forskningsemnerne om 'Psi-calculi in Isabelle'. Sammen danner de et unikt fingeraftryk.

Citationsformater