Speaker / Predavač : Dr. Silvia Likavec
Title / Naslov: On the semantics of untyped calculus of Curien and Herbelin
Abstract / Rezime:
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 the two 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.