A CPS-semantics for a typed lambda-calculus of exception handling with fixed-point

Catherine Pilière 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00098699
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:17:50 AM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM
Long-term archiving on : Wednesday, March 29, 2017 - 12:36:33 PM

Identifiers

  • HAL Id : inria-00098699, version 1

Collections

Citation

Catherine Pilière. A CPS-semantics for a typed lambda-calculus of exception handling with fixed-point. ESSLLI'98, 1998, none, 12 p. ⟨inria-00098699⟩

Share

Metrics

Record views

96

Files downloads

46