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.
|Title of host publication||Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming|
|Place of Publication||New York, NY, USA|
|Number of pages||9|
|Publication status||Published - 2003|
- classical realizability
- control structures
- disjunctive normal forms