On the Algebra of Structural Contexts

François Lamarche 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We discuss a general way of defining contexts in linear logic, based on the observation that linear universal algebra can be symmetrized by assigning an additional variable to represent the output of a term. We give two approaches to this, a syntactical one based on a new, reversible notion of term, and an algebraic one based on a simple generalization of typed operads. We relate these to each other and to known examples of logical systems, and show new examples, in particular discussing the relationship between intuitionistic and classical systems. We then present a general framework for extracting deductive system from a given theory of contexts, and prove that all these systems have cut-elimination by the means of a generic argument.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2003, 51 p
Liste complète des métadonnées

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

Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:13:55
Dernière modification le : mardi 25 octobre 2016 - 17:01:38
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 11:44:47



  • HAL Id : inria-00099461, version 1



François Lamarche. On the Algebra of Structural Contexts. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2003, 51 p. 〈inria-00099461〉



Consultations de
la notice


Téléchargements du document