Encoding transition systems in sequent calculus

DOI10.1016/S0304-3975(01)00168-2zbMath1028.68095MaRDI QIDQ1398474

Raymond McDowell, Catuscia Palamidessi, Dale A. Miller

Publication date: 29 July 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

Linear logicBisimulationDefinitionsLogic specificationTransition systems

Mathematics Subject Classification ID

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

Related Items

Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols ⋮ Extracting Proofs from Tabled Proof Search ⋮ Nominal abstraction ⋮ Cut elimination for a logic with induction and co-induction ⋮ Relating State-Based and Process-Based Concurrency through Linear Logic ⋮ Relating reasoning methodologies in linear logic and process algebra ⋮ Relating state-based and process-based concurrency through linear logic (full-version) ⋮ Constructing weak simulations from linear implications for processes with private names ⋮ Encoding Generic Judgments ⋮ A proof theory for model checking

Uses Software

• ML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Forum: A multiple-conclusion specification logic
• A calculus of communicating systems
• Partial inductive definitions
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Cut-elimination for a logic with definitions and induction
• Contributions to the Theory of Logic Programming
• A Proof-Theoretic Approach to Logic Programming
• A Complete Axiomatization of the Three valued Completion of Logic Programs
• From operational semantics to abstract machines
• Logic programming and negation: A survey

This page was built for publication: Encoding transition systems in sequent calculus