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.
Type de document :
Communication dans un congrès
Michel Parigot and Lutz Straßburger. Structures and Deduction 2009, Jul 2009, Bordeaux, France. pp.117-133, 2009, 〈http://www.lix.polytechnique.fr/~lutz/orgs/sd09-proc.pdf〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00440875
Contributeur : Novak Novakovic <>
Soumis le : dimanche 13 décembre 2009 - 01:26:40
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00440875, version 1

Collections

Citation

François Lamarche, Novak Novakovic. Two Denotational Interpretations of Proofs in Classical Logic. Michel Parigot and Lutz Straßburger. Structures and Deduction 2009, Jul 2009, Bordeaux, France. pp.117-133, 2009, 〈http://www.lix.polytechnique.fr/~lutz/orgs/sd09-proc.pdf〉. 〈inria-00440875〉

Partager

Métriques

Consultations de la notice

134