On categorical models of classical logic and the Geometry of Interaction

DOI10.1017/S0960129507006287zbMath1129.03038MaRDI QIDQ5430139

Carsten Führmann, David J. Pym

Publication date: 12 December 2007

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

Boolean latticesproof netmultiplicative linear logicclassical sequent calculusclassical categoryDummett categorysymmetric linearly distributive category

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (2)

Deep inference and probabilistic coherence spaces ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Linear logic
• Weakly distributive categories
• A categorical model for the geometry of interaction
• Natural deduction and coherence for weakly distributive categories
• Coherence for compact closed categories
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• The structure of multiplicatives
• Glueing and orthogonality for models of linear logic
• Feedback for linearly distributive categories: Traces and fixpoints
• Linearly distributive functors
• Untersuchungen über das logische Schliessen. I
• A symmetric lambda calculus for classical program extraction
• Order-enriched categorical models of the classical sequent calculus
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• Proof Nets for Classical Logic
• Geometry of Interaction and linear combinatory algebras
• On the semantics of classical disjunction
• Proof theory in the abstract

This page was built for publication: On categorical models of classical logic and the Geometry of Interaction