LIPIcs.TYPES.2013.150.pdf
- Filesize: 0.64 MB
- 19 pages
Document
A Hybrid Linear Logic for Constrained Transition Systems
Authors
-
Part of:
Volume:
19th International Conference on Types for Proofs and Programs (TYPES 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2014-07-25
Cite AsGet BibTex
Joëlle Despeyroux and Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 150-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.TYPES.2013.150
https://doi.org/10.4230/LIPIcs.TYPES.2013.150
Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus.
Keywords
- Linear logic
- hybrid logic
- stochastic pi-calculus
- focusing
- adequacy
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads