A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
From MaRDI portal
Publication:4457837
DOI10.1017/S0956796802004653zbMath1096.68679OpenAlexW2125412310MaRDI QIDQ4457837
Daniel Hirschkoff, Christine Röckl
Publication date: 17 March 2004
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796802004653
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
ASP\(_{\text{fun}}\) : a typed functional active object calculus ⋮ Psi-calculi in Isabelle ⋮ Psi-calculi in Isabelle ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle
Uses Software
This page was built for publication: A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
