A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations

DOI10.1016/S1571-0661(04)00276-2zbMath1268.68053OpenAlexW2031176814MaRDI QIDQ2841231

Christine Röckl

Publication date: 24 July 2013

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

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)00276-2

Mathematics Subject Classification ID

Related Items (3)

\(\mathrm{HO}\pi\) in Coq ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/ZF
• HOL

Cites Work

• A calculus of mobile processes. II
• \(\pi\)-calculus in (Co)inductive-type theory
• Objects in the \(\pi\)-calculus
• Some lambda calculus and type theory formalized
• Functions as processes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations