Proof search specifications of bisimulation and modal logics for the π-calculus

DOI10.1145/1656242.1656248zbMath1351.68186OpenAlexW2104680392MaRDI QIDQ2946601

Alwen Tiu, Dale A. Miller

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1656242.1656248

zbMATH Keywords

bisimulation\(\pi\)-calculusmodal logicsproof searchhigher-order abstract syntaxgeneric judgments\(\lambda\)-tree syntax\(\nabla\)-quantifier

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (17)

A Logical Encoding of Timed $$\pi $$-Calculus ⋮ Extracting Proofs from Tabled Proof Search ⋮ HOCore in Coq ⋮ Nominal abstraction ⋮ αCheck: A mechanized metatheory model checker ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Cut elimination for a logic with induction and co-induction ⋮ Unnamed Item ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ On the Role of Names in Reasoning about λ-tree Syntax Specifications ⋮ Constructing weak simulations from linear implications for processes with private names ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ Divergence and unique solution of equations ⋮ A proof theory for model checking ⋮ Unnamed Item

This page was built for publication: Proof search specifications of bisimulation and modal logics for the π-calculus