EMIS ELibM Electronic Journals Publications de l'Institut Mathématique, Nouvelle Série
Vol. 92(106), pp. 79–95 (2012)

Previous Article

Next Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home

EMIS Home

Pick a mirror

 		 

ON SEMANTICS OF A TERM CALCULUS FOR CLASSICAL LOGIC

Silvia Likavec and Pierre Lescanne

Dipartimento di Informatica, Universita di Torino, Italy; University of Lyon, Ecole Normal Supérieure de Lyon, France

Abstract: The calculus of Curien and Herbelin was introduced to provide the Curry–Howard correspondence for classical logic. The terms of this calculus represent derivations in the sequent calculus proof system and reduction reflects the process of cut-elimination. This work investigates some properties of two well-behaved subcalculi of untyped calculus of Curien and Herbelin, closed under the call-by-name and the call-by-value reduction, respectively. Continuation semantics is given using the category of negated domains and Moggi's Kleisli category over predomains for the continuation monad. Soundness theorems are given for both versions thus relating operational and denotational semantics. A thorough overview of the work on continuation semantics is given.

Classification (MSC2000): 03B40; 03B70; 18C50; 68N18

Full text of the article: (for faster download, first choose a mirror)

Electronic fulltext finalized on: 8 Nov 2012. This page was last modified: 19 Nov 2012.

© 2012 Mathematical Institute of the Serbian Academy of Science and Arts
© 2012 FIZ Karlsruhe / Zentralblatt MATH for the EMIS Electronic Edition