A CPS-semantics for a typed lambda-calculus of exception handling with fixed-point
Résumé
We propose to add a fixed-point combinator to a lambda- calculus of exception handling whose type system corresponds to classical logic through the Curry-Howard isomorphism. To this end, we here give a CPS-semantics to the calculus and show that for non-exceptional terms, this semantics possesses the property of computational adequacy.