Disjunctive Normal Forms and Local Exceptions

摘要

All classical λ-terms typable with disjunctive normal forms are shown to share a common computational behavior: they implement a local exception handling mechanism whose exact workings depend on the tautology. Equivalent and more efficient control com-binators are described through a specialized sequent calculus and shown to be correct.