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.
['Emmanuel Beffara', 'Vincent Danos']
Disjunctive normal forms and local exceptions