Geodesic
On Semantics of a Term Calculus for Classical Logic
Publications de l'Institut Mathématique, _N_S_92 (2012) no. 106, p. 79 .

Voir la notice de l'article provenant de 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 },
     publisher = {mathdoc},
     volume = {_N_S_92},
     number = {106},
     year = {2012},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/PIM_2012_N_S_92_106_a5/}
}
TY  - JOUR
AU  - Silvia Likavec
AU  - Pierre Lescanne
TI  - On Semantics of a Term Calculus for Classical Logic
JO  - Publications de l'Institut Mathématique
PY  - 2012
SP  - 79 
VL  - _N_S_92
IS  - 106
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PIM_2012_N_S_92_106_a5/
LA  - en
ID  - PIM_2012_N_S_92_106_a5
ER  - 
%0 Journal Article
%A Silvia Likavec
%A Pierre Lescanne
%T On Semantics of a Term Calculus for Classical Logic
%J Publications de l'Institut Mathématique
%D 2012
%P 79 
%V _N_S_92
%N 106
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PIM_2012_N_S_92_106_a5/
%G en
%F 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/