On Semantics of a Term Calculus for Classical Logic
Publications de l'Institut Mathématique, _N_S_92 (2012) no. 106, p. 79
Cet article a éte moissonné depuis la source eLibrary of Mathematical Institute of the Serbian Academy of Sciences and Arts
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 :
03B40 03B70 18C50 68N18
@article{PIM_2012_N_S_92_106_a5,
author = {Silvia Likavec and Pierre Lescanne},
title = {On {Semantics} of a {Term} {Calculus} for {Classical} {Logic}},
journal = {Publications de l'Institut Math\'ematique},
pages = {79 },
year = {2012},
volume = {_N_S_92},
number = {106},
language = {en},
url = {http://geodesic.mathdoc.fr/item/PIM_2012_N_S_92_106_a5/}
}
Silvia Likavec; Pierre Lescanne. On Semantics of a Term Calculus for Classical Logic. Publications de l'Institut Mathématique, _N_S_92 (2012) no. 106, p. 79 . http://geodesic.mathdoc.fr/item/PIM_2012_N_S_92_106_a5/