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
Formalising the pi-calculus using nominal logic
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (mobility)
2007 (English)In: FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS / [ed] Seidl, H, 2007, 63-77 p.Conference paper, Published paper (Refereed)
Abstract [en]

We formalise the pi-calculus using the nominal datatype package, a package based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely following the intuitive arguments found in manual proofs. In this way we have covered many of the standard theorems of bisimulation equivalence and congruence, both late and early, and both strong and weak in a unison manner. We thus provide one of the most extensive formalisations of a process calculus ever done inside a theorem prover.

A significant gain in our formulation is that agents are identified up to alpha-equivalence, thereby greatly reducing the arguments about bound names. This is a normal strategy for manual proofs about the pi-calculus, but that kind of hand waving has previously been difficult to incorporate smoothly in an interactive theorem prover. We show how the nominal logic formalism and its support in Isabelle accomplishes this and thus significantly reduces the tedium of conducting completely formal proofs. This improves on previous work using weak higher order abstract syntax since we do not need extra assumptions to filter out exotic terms and can keep all arguments within a familiar first-order logic.

Place, publisher, year, edition, pages
2007. 63-77 p.
Series
LECTURE NOTES IN COMPUTER SCIENCE, ISSN 0302-9743 ; 4423
Keyword [en]
pi-calculus, interactive theorem provers, Isabelle
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:uu:diva-26614ISI: 000246296000006ISBN: 978-3-540-71388-3 (print)OAI: oai:DiVA.org:uu-26614DiVA: diva2:54388
Available from: 2007-04-13 Created: 2007-04-13 Last updated: 2011-04-14Bibliographically approved

Open Access in DiVA

No full text

Other links

http://www.it.uu.se/research/group/mobility/theorem/nompi.pdf

Authority records BETA

Bengtson, JesperParrow, Joachim

Search in DiVA

By author/editor
Bengtson, JesperParrow, Joachim
By organisation
Computing Science
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 476 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