Psi-calculi in Isabelle

DOI10.1007/978-3-642-03359-9_9zbMath1252.68247OpenAlexW1499941466MaRDI QIDQ5895110

Jesper Bengtson, Joachim Parrow

Publication date: 20 October 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_9

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Related Items

Mechanizing a process algebra for network protocols, A canonical locally named representation of binding, Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants, HOCore in Coq, Computing strong and weak bisimulations for psi-calculi, Psi-calculi in Isabelle, General Bindings and Alpha-Equivalence in Nominal Isabelle

Uses Software

• Isabelle
• Nominal Isabelle
• Psi-calculi

Cites Work

• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Nominal techniques in Isabelle/HOL
• \(\pi\)-calculus in (Co)inductive-type theory
• Nominal logic, a first order theory of names and binding
• Psi-calculi: a framework for mobile processes with nominal data and logic
• Engineering formal metatheory
• Nominal Inversion Principles
• Barendregt’s Variable Convention in Rule Inductions
• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• Mobile values, new names, and secure communication
• Open Bisimulation for the Concurrent Constraint Pi-Calculus
• Types for Proofs and Programs
• Formalising the π-Calculus Using Nominal Logic