Formalising the π-Calculus Using Nominal Logic

DOI10.1007/978-3-540-71389-0_6MaRDI QIDQ5758048zbMATH OpenOpenAlexFDO

Authors Jesper Bengtson, Joachim Parrow

Publication date 7 September 2007

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71389-0_6

zbMATH Keywords

bisimulation equivalenceimplementation in Isabelle/HOLinteractive theorem provingnominal logicpi-calculus

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Formalising the pi-calculus using nominal logic
• scientific article; zbMATH DE number 1082078
• scientific article; zbMATH DE number 1863387
• A completeness proof for bisimulation in the pi-calculus using Isabelle
• Implementing Spi Calculus Using Nominal Techniques

Cited in

(16)

• -calculus in (Co)inductive-type theory
• \( \pi\) with leftovers: a mechanisation in Agda
• A first-order syntax for the -calculus in Isabelle/HOL using permutations
• A completeness proof for bisimulation in the pi-calculus using Isabelle
• scientific article; zbMATH DE number 2185678 (Why is no real title available?)
• Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
• Mechanizing the metatheory of mini-XQuery
• Formalising the pi-calculus using nominal logic
• Implementing Spi Calculus Using Nominal Techniques
• ASP\(_{\text{fun}}\) : a typed functional active object calculus
• scientific article; zbMATH DE number 1082078 (Why is no real title available?)
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
• scientific article; zbMATH DE number 1863387 (Why is no real title available?)
• Psi-calculi in Isabelle
• Psi-calculi in Isabelle
• Nominal techniques in Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Formalising the π-Calculus Using Nominal Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5758048)