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 metadatas

https://hal.inria.fr/inria-00440875
Contributor : Novak Novakovic <>
Submitted on : Sunday, December 13, 2009 - 1:26:40 AM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM

Identifiers

  • HAL Id : inria-00440875, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

148