Disjunctive Normal Forms and Local Exceptions

Emmanuel Beffara; Vincent Danos

doi:10.1145/944705.944724

Disjunctive Normal Forms and Local Exceptions

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	ICFP '03 Proceedings of the eighth ACM SIGPLAN international conference on Functional programming
Publisher	ACM
Pages	203-211
Number of pages	9
ISBN (Print)	1-58113-756-7
DOIs	https://doi.org/10.1145/944705.944724
Publication status	Published - Aug 2003

Keywords / Materials (for Non-textual outputs)

classical realizability
control structures
disjunctive normal forms

Access to Document

10.1145/944705.944724

Cite this

@inproceedings{2440e6cf2cd34ef7910473ff820fccd6,

title = "Disjunctive Normal Forms and Local Exceptions",

abstract = "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. ",

keywords = "classical realizability, control structures, disjunctive normal forms",

author = "Emmanuel Beffara and Vincent Danos",

year = "2003",

month = aug,

doi = "10.1145/944705.944724",

language = "English",

isbn = "1-58113-756-7",

pages = "203--211",

booktitle = "ICFP '03 Proceedings of the eighth ACM SIGPLAN international conference on Functional programming",

publisher = "ACM",

}

TY - GEN

T1 - Disjunctive Normal Forms and Local Exceptions

AU - Beffara, Emmanuel

AU - Danos, Vincent

PY - 2003/8

Y1 - 2003/8

N2 - 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.

AB - 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.

KW - classical realizability

KW - control structures

KW - disjunctive normal forms

U2 - 10.1145/944705.944724

DO - 10.1145/944705.944724

M3 - Conference contribution

SN - 1-58113-756-7

SP - 203

EP - 211

BT - ICFP '03 Proceedings of the eighth ACM SIGPLAN international conference on Functional programming

PB - ACM

ER -

Disjunctive Normal Forms and Local Exceptions

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this