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 combinators are described through a specialized sequent calculus and shown to be correct.
disjunctive normal forms control structures classical realizability