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
Conference papers

Two Denotational Interpretations of Proofs in Classical Logic

François Lamarche 1 Novak Novakovic 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper we present and compare two interpretations of classical logic proofs in a category of posets and relations, and relate their behavior to proof nets, extracting meaningful invariants of proofs. We show that at least one of these interpretation cannot have anything to do with the Curry-Howard correspondence.
Document type :
Conference papers
Complete list of metadata

Contributor : Novak Novakovic Connect in order to contact the contributor
Submitted on : Sunday, December 13, 2009 - 1:26:40 AM
Last modification on : Friday, February 4, 2022 - 3:30:15 AM


  • HAL Id : inria-00440875, version 1



François Lamarche, Novak Novakovic. Two Denotational Interpretations of Proofs in Classical Logic. Structures and Deduction 2009, Jul 2009, Bordeaux, France. pp.117-133. ⟨inria-00440875⟩



Record views