Encoding transition systems in sequent calculus

DOI10.1016/S0304-3975(01)00168-2MaRDI QIDQ1398474zbMATH OpenFDO

Authors Raymond McDowell, Catuscia Palamidessi, Dale 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)

Recommendations

• scientific article; zbMATH DE number 1231524
• scientific article; zbMATH DE number 2152687
• scientific article; zbMATH DE number 1950250
• A hybrid linear logic for constrained transition systems
• A formal framework for specifying sequent calculus proof systems

Cites work

• scientific article; zbMATH DE number 4035108 (Why is no real title available?)
• scientific article; zbMATH DE number 4092734 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A Complete Axiomatization of the Three valued Completion of Logic Programs
• A Proof-Theoretic Approach to Logic Programming
• A calculus of communicating systems
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Contributions to the Theory of Logic Programming
• Cut-elimination for a logic with definitions and induction
• Forum: A multiple-conclusion specification logic
• From operational semantics to abstract machines
• Linear logic
• Logic programming and negation: A survey
• Partial inductive definitions

Cited in

(17)

• Attributed transition systems with hidden transitions
• Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
• A hybrid linear logic for constrained transition systems
• Cut elimination for a logic with induction and co-induction
• Logic of transition systems
• Modal transition system encoding of featured transition systems
• Nominal abstraction
• A proof theory for model checking
• Extracting proofs from tabled proof search
• Constructing weak simulations from linear implications for processes with private names
• 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)
• Encoding generic judgments: preliminary results
• Macrotransducers and applicative systems for partially continuous functions
• scientific article; zbMATH DE number 1361475 (Why is no real title available?)
• scientific article; zbMATH DE number 1512706 (Why is no real title available?)

Describes a project that uses

Uses Software

• ML

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

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