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

https://hal.inria.fr/hal-01285039
Contributor : Joelle Despeyroux <>
Submitted on : Tuesday, March 8, 2016 - 2:40:25 PM
Last modification on : Saturday, May 1, 2021 - 3:38:49 AM
Long-term archiving on: : Sunday, November 13, 2016 - 10:37:51 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

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

Collections

Citation

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⟩

Share

Metrics

Record views

251

Files downloads

83