A Hybrid Linear Logic for Constrained Transition Systems

Joelle Despeyroux 1 Kaustuv Chaudhuri 2
1 Inria - Institut National de Recherche en Informatique et en Automatique
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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
Type de document :
Communication dans un congrès
LIPIcs. TYPES'2013, Apr 2013, Toulouse, France. Post-proceedings of TYPES'2013, 19th Intl Conference on Types for Proofs and Programs, LIPIcs., 26, pp.150-168, 2014
Liste complète des métadonnées
https://hal.inria.fr/hal-01285039
Contributeur : Joelle Despeyroux <>
Soumis le : mardi 8 mars 2016 - 14:40:25
Dernière modification le : jeudi 10 mai 2018 - 02:06:33
Document(s) archivé(s) le : dimanche 13 novembre 2016 - 10:37:51

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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

Collections

X | LIX | INRIA | X-LIX | PARISTECH | X-DEP-INFO

Citation

Joelle Despeyroux, Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. LIPIcs. TYPES'2013, Apr 2013, Toulouse, France. Post-proceedings of TYPES'2013, 19th Intl Conference on Types for Proofs and Programs, LIPIcs., 26, pp.150-168, 2014. 〈hal-01285039〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

170

Téléchargements de fichiers

36

Contact


archive-ouverte@inria.fr