From Proof nets to the Free *-Autonomous Categories

François Lamarche 1 Lutz Strassburger 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In the first part of this paper we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-free multiplicative proof nets. A linking is no longer a set of axiom links but a tree in which the axiom links are subtrees. These trees will be identified according to an equivalence relation based on a simple form of graph rewriting. We show the standard results of sequentialization and strong normalization of cut elimination. In the second part of the paper we show that the identifications enforced on proofs are such that the class of two-conclusion proof nets defines the free *-autonomous category.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2006, 2 (4:3), 44 p. 〈10.2168/LMCS-2(4:3) 2006〉
Liste complète des métadonnées

Littérature citée [58 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00099865
Contributeur : Publications Loria <>
Soumis le : jeudi 16 novembre 2006 - 14:41:52
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:46:50

Fichier

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

Identifiants

Collections

Citation

François Lamarche, Lutz Strassburger. From Proof nets to the Free *-Autonomous Categories. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2006, 2 (4:3), 44 p. 〈10.2168/LMCS-2(4:3) 2006〉. 〈inria-00099865v2〉

Partager

Métriques

Consultations de la notice

225

Téléchargements de fichiers

191