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 metadatas

Cited literature [68 references]  Display  Hide  Download

https://hal.inria.fr/inria-00099461
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:13:55 AM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM
Long-term archiving on : Friday, November 25, 2016 - 11:44:47 AM

Identifiers

  • HAL Id : inria-00099461, version 1

Collections

Citation

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

Share

Metrics

Record views

353

Files downloads

139