Disjunctive Normal Forms and Local Exceptions

Emmanuel Beffara, Vincent Danos

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationICFP '03 Proceedings of the eighth ACM SIGPLAN international conference on Functional programming
Number of pages9
ISBN (Print)1-58113-756-7
Publication statusPublished - Aug 2003


  • classical realizability
  • control structures
  • disjunctive normal forms


Dive into the research topics of 'Disjunctive Normal Forms and Local Exceptions'. Together they form a unique fingerprint.

Cite this