HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [68 references]  Display  Hide  Download

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:13:55 AM
Last modification on : Friday, February 4, 2022 - 3:30:48 AM
Long-term archiving on: : Friday, November 25, 2016 - 11:44:47 AM


  • 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⟩



Record views


Files downloads