A System of Interaction and Structure IV: The Exponentials and Decomposition

Lutz Straßburger 1 Alessio Guglielmi 2
1 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
2 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. System NEL is Turing-complete, it is able to directly express process algebra sequential composition and it faithfully models causal quantum evolution. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2011, 12 (4), pp.23. 〈10.1145/1970398.1970399〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00441214
Contributeur : Lutz Straßburger <>
Soumis le : mercredi 28 janvier 2015 - 19:20:29
Dernière modification le : jeudi 10 mai 2018 - 02:07:00
Document(s) archivé(s) le : mercredi 29 avril 2015 - 11:35:47

Fichier

SIS-IV.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Lutz Straßburger, Alessio Guglielmi. A System of Interaction and Structure IV: The Exponentials and Decomposition. ACM Transactions on Computational Logic, Association for Computing Machinery, 2011, 12 (4), pp.23. 〈10.1145/1970398.1970399〉. 〈inria-00441214〉

Partager

Métriques

Consultations de la notice

201

Téléchargements de fichiers

93