A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle

DOI10.1016/j.entcs.2007.08.017zbMath1278.68212OpenAlexW1967451324MaRDI QIDQ2871830

Joachim Parrow, Jesper Bengtson

Publication date: 10 January 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.08.017

zbMATH Keywords

bisimulationaxiomatizationpi-calculusIsabelletheorem provers

Mathematics Subject Classification ID

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

Related Items (2)

Unnamed Item ⋮ Unique solutions of contractions, CCS, and their HOL formalisation

Uses Software

• Isabelle
• Isabelle/HOL

Cites Work

• A calculus of mobile processes. II
• \(\pi\)-calculus in (Co)inductive-type theory
• Isabelle/HOL. A proof assistant for higher-order logic
• Algebraic laws for nondeterminism and concurrency
• Metamathematics, Machines and Gödel's Proof
• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• Formalising the π-Calculus Using Nominal Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle