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

ON SEMANTICS OF A TERM CALCULUS FOR CLASSICAL LOGICSilvia Likavec and Pierre LescanneDipartimento di Informatica, Universita di Torino, Italy; University of Lyon, Ecole Normal Supérieure de Lyon, FranceAbstract: 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 cutelimination. This work investigates some properties of two wellbehaved subcalculi of untyped calculus of Curien and Herbelin, closed under the callbyname and the callbyvalue 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
