Proof-relevant π-calculus: a constructive account of concurrency and causality
From MaRDI portal
Publication:4691184
DOI10.1017/S096012951700010XzbMath1400.68142arXiv1604.04575MaRDI QIDQ4691184
Publication date: 19 October 2018
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1604.04575
Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (3)
Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ Unnamed Item ⋮ \(\mathrm{HO}\pi\) in Coq
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
- Concurrent transition systems
- A fully abstract semantics for causality in the \(\pi\)-calculus
- A calculus of communicating systems
- A calculus of mobile processes. I
- Non-interleaving semantics for mobile processes
- Flow models of distributed computations: Three equivalent semantics for CCS
- Typing correspondence assertions for communication protocols
- \(\pi\)-calculus in (Co)inductive-type theory
- Rigid Families for CCS and the $$\pi $$ -calculus
- Homotopical patch theory
- A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations
- A Coq Library for Verification of Concurrent Programs
- Specifying Properties of Concurrent Computations in CLF
- Proof search specifications of bisimulation and modal logics for the π-calculus
- Formalising the pi-calculus using nominal logic
- Reversing Higher-Order Pi
- Dependently Typed Programming in Agda
- A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
- Residual theory in λ-calculus: a formal development
- Proof Pearl: Abella Formalization of λ-Calculus Cube Property
- Abella: A System for Reasoning about Relational Specifications
- CONCUR 2004 - Concurrency Theory
- Consistency of the theory of contexts
This page was built for publication: Proof-relevant π-calculus: a constructive account of concurrency and causality
