Psi-calculi in Isabelle
From MaRDI portal
Publication:5890661
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
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
