Technical Report TR608:
A ProofTheoretic Foundation of Abortive Continuations (Extended version)
Zena M. Ariola, Hugo Herbelin, and Amr Sabry
(Feb 2005), 43 pages pages
[This is an extended version of the conference article "Minimal Classical Logic and Control Operators, Zena M. Ariola & Hugo Herbelin, Thirtieth International Colloquium on Automata, Languages & Programming, 2003, SpringerVerlag, LNCS 2719, pgs. 871885."]
 Abstract:

We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce's law without enforcing Ex Falso Quodlibet. We show that a natural implementation of this logic is Parigot's classical natural deduction. We then move on to the computational side and emphasize that Parigot's lambdamu corresponds to minimal classical logic. A continuation constant must be added to lambdamu to get full classical logic. We then map the extended lambdamu to a new theory of control, lambdaCminustop, which extends Felleisen's reduction theory. The new theory lambdaCminustop distinguishes between aborting and throwing to a continuation and is in correspondence with a refined version of Prawitz's natural deduction system.
 Available as:
