Formalising the pi-calculus using nominal logic

DOI10.2168/LMCS-5(2:16)2009zbMath1168.68030MaRDI QIDQ3395094

Jesper Bengtson, Joachim Parrow

Publication date: 20 August 2009

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

nominal logicpi-calculusinteractive theorem provingbisimulation equivalenceimplementation in Isabelle/HOL

Mathematics Subject Classification ID

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

Related Items (12)

On the Expressiveness of Symmetric Communication ⋮ Unnamed Item ⋮ Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ Nominal Sets in Agda - A Fresh and Immature Mechanization ⋮ Proofs about Network Communication: For Humans and Machines ⋮ Unnamed Item ⋮ Unique solutions of contractions, CCS, and their HOL formalisation ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ Constructing weak simulations from linear implications for processes with private names ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Coverability Synthesis in Parametric Petri Nets

Uses Software

• Isabelle/HOL
• MWB
• Isar

This page was built for publication: Formalising the pi-calculus using nominal logic