Skip to Main content Skip to Navigation
Conference papers

A Hybrid Linear Logic for Constrained Transition Systems

Joelle Despeyroux 1 Kaustuv Chaudhuri 2 
1 AxIS - Usage-centered design, analysis and improvement of information systems
CRISAM - Inria Sophia Antipolis - Méditerranée , Inria Paris-Rocquencourt
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Joelle Despeyroux Connect in order to contact the contributor
Submitted on : Tuesday, March 8, 2016 - 2:40:25 PM
Last modification on : Saturday, June 25, 2022 - 9:10:01 PM
Long-term archiving on: : Sunday, November 13, 2016 - 10:37:51 AM


Files produced by the author(s)


  • HAL Id : hal-01285039, version 1
  • ARXIV : 1603.02641



Joelle Despeyroux, Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. TYPES 2013 - 19th International Conference on Types for Proofs and Programs, Apr 2013, Toulouse, France. pp.150-168. ⟨hal-01285039⟩



Record views


Files downloads