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

DOI10.1145/1656242.1656248MaRDI QIDQ2946601zbMATH OpenOpenAlexFDO

Authors Alwen Tiu, Dale 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

\(\lambda\)-tree syntax\(\nabla\)-quantifier\(\pi\)-calculusbisimulationgeneric judgmentshigher-order abstract syntaxmodal logicsproof search

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)

Recommendations

• A proof search specification of the -calculus
• Computer Science Logic
• CONCUR 2005 – Concurrency Theory
• A theory of bisimulation for the -calculus
• Modal logics for nominal transition systems

Cited in

(29)

• Cut elimination for a logic with induction and co-induction
• Mechanized metatheory revisited
• A proof theory for model checking
• On the role of names in reasoning about -tree syntax specifications
• A proof search specification of the -calculus
• Full Hybrid μ-Calculus, Its Bisimulation Invariance and Application to Argumentation
• Extracting proofs from tabled proof search
• HOCore in Coq
• A logical encoding of timed \(\pi\)-calculus
• scientific article; zbMATH DE number 1223732 (Why is no real title available?)
• αCheck: A mechanized metatheory model checker
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• A proof theory for model checking: an extended abstract
• POPLMark reloaded: mechanizing proofs by logical relations
• A characterisation of open bisimilarity using an intuitionistic modal logic
• A characterisation of open bisimilarity using an intuitionistic modal logic
• Constructing weak simulations from linear implications for processes with private names
• A case study in programming coinductive proofs: Howe's method
• A proof theoretic approach to operational semantics
• Computer Science Logic
• Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus
• CONCUR 2005 – Concurrency Theory
• Nominal abstraction
• Mechanized metatheory revisited: an extended abstract (invited paper)
• Proof-relevant -calculus
• Modal logics for mobile processes revisited
• Open bisimilarity for the -calculus with mismatch
• Barendregt's theory of the -calculus, refreshed and formalized

This page was built for publication: Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946601)