Psi-calculi in Isabelle

DOI10.1007/S10817-015-9336-2zbMath1356.68175OpenAlexW1149872217MaRDI QIDQ5890661

Jesper Bengtson, Tjark Weber, Joachim Parrow

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9336-2

zbMATH Keywords

process calculinominal logicpsi-calculiproof assistantsmechanisation

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mechanization of proofs and logical operations (03B35)

Related Items (9)

Translation of CCS into CSP, correct up to strong bisimulation ⋮ A formalized general theory of syntax with bindings ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Psi-calculi revisited: connectivity and compositionality ⋮ Proofs about Network Communication: For Humans and Machines ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Psi-calculi ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Unnamed Item

Uses Software

• Coq
• Isabelle
• ML
• Isabelle/HOL
• Isabelle/Isar
• Isar
• HOL
• PoplMark
• Paco
• Nominal Isabelle
• CC-Pi
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Nominal techniques in Isabelle/HOL
• A calculus of communicating systems
• The lambda calculus, its syntax and semantics
• A calculus of mobile processes. I
• A calculus for cryptographic protocols: The spi calculus
• \(\pi\)-calculus in (Co)inductive-type theory
• Nominal logic, a first order theory of names and binding
• The locally nameless representation
• A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract)
• The power of parameterization in coinductive proof
• Psi-calculi: a framework for mobile processes with nominal data and logic
• Broadcast Psi-calculi with an Application to Wireless Protocols
• Engineering formal metatheory
• Implementing Spi Calculus Using Nominal Techniques
• A Short Presentation of Coq
• A Brief Overview of HOL4
• The Isabelle Framework
• Nominal Inversion Principles
• Barendregt’s Variable Convention in Rule Inductions
• Process algebra for synchronous communication
• Communicating sequential processes
• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• Mobile values, new names, and secure communication
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• Higher-order psi-calculi
• A New Foundation for Nominal Isabelle
• CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements
• Formalising the π-Calculus Using Nominal Logic
• An Unsolvable Problem of Elementary Number Theory
• General Bindings and Alpha-Equivalence in Nominal Isabelle
• Psi-calculi in Isabelle

This page was built for publication: Psi-calculi in Isabelle