A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis

DOI10.1017/S0956796802004653MaRDI QIDQ4457837zbMATH OpenOpenAlexFDO

Authors Christine Röckl, Daniel Hirschkoff

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

Mathematics Subject Classification ID

Theory of programming languages (68N15) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 1701361
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Higher-order abstract syntax in Isabelle/HOL
• scientific article; zbMATH DE number 2185657
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq

Cited in

(8)

• A completeness proof for bisimulation in the pi-calculus using Isabelle
• scientific article; zbMATH DE number 1701361 (Why is no real title available?)
• Psi-calculi in Isabelle
• ASP\(_{\text{fun}}\) : a typed functional active object calculus
• \(\mathrm{HO}\pi\) in Coq
• Higher-order abstract syntax in Isabelle/HOL
• Psi-calculi in Isabelle
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Twelf

This page was built for publication: A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis

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