uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Psi-Calculi in Isabelle
IT Univ Copenhagen, Copenhagen, Denmark..
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2016 (English)In: Journal of automated reasoning, ISSN 0168-7433, E-ISSN 1573-0670, Vol. 56, no 1, 1-47 p.Article in journal (Refereed) Published
Resource type
Text
Abstract [en]

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.

Place, publisher, year, edition, pages
2016. Vol. 56, no 1, 1-47 p.
Keyword [en]
Psi-calculi, Process calculi, Proof assistants, Nominal logic, Mechanisation
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-275571DOI: 10.1007/s10817-015-9336-2ISI: 000367884100001OAI: oai:DiVA.org:uu-275571DiVA: diva2:900459
Available from: 2016-02-04 Created: 2016-02-04 Last updated: 2017-11-30Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Parrow, JoachimWeber, Tjark

Search in DiVA

By author/editor
Parrow, JoachimWeber, Tjark
By organisation
Computing Science
In the same journal
Journal of automated reasoning
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 246 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf