Proof-relevant π-calculus: a constructive account of concurrency and causality

DOI10.1017/S096012951700010XzbMath1400.68142arXiv1604.04575MaRDI QIDQ4691184

James Cheney, Roly Perera

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

Mathematics Subject Classification ID

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

• Abella
• Agda
• Nominal Isabelle
• CLF

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