Exception Handling and Classical Logic

We present lambda(try), an extension of the lambda-calculus with named exception handling, via try, throw and catch, and present a basic notion of type assignment expressing recoverable exception handling and show that it is sound. We define an interpretation for lambda(try) to Parigot's lambda mu-calculus, and show that reduction (both lazy and call by value) is preserved by the interpretation. We will show that also types assignable in the basic system are preserved by the interpretation. We will then add a notion of total failure through halt that escapes applicative contexts without being caught by a handler, and show that we can interpret this in lambda mu when adding top as destination. We will argue that introducing handlers for halt will break the relation with lambda mu. We will conclude the paper by showing that it is possible to add handlers for program failure by introducing panic and dedicated handlers to lambda(try). We will need to extend the language with a conditional construct that is typed in a non-traditional way, that cannot be expressed in lambda mu or logic. This will allow both recoverable exceptions and total failure, dealt with by handlers; we will show a non-standard soundness result for this system.