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.
https://hal.inria.fr/hal-01285039 Contributor : Joelle DespeyrouxConnect 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
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⟩