A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
DOI10.1017/S0956796802004653zbMATH Open1096.68679OpenAlexW2125412310MaRDI QIDQ4457837FDOQ4457837
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
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
Theory of programming languages (68N15) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cited In (8)
- ASP\(_{\text{fun}}\) : a typed functional active object calculus
- Psi-calculi in Isabelle
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- \(\mathrm{HO}\pi\) in Coq
- A completeness proof for bisimulation in the pi-calculus using Isabelle
- Psi-calculi in Isabelle
- Title not available (Why is that?)
- Higher-order abstract syntax in Isabelle/HOL
Uses Software
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)
