Computer Science

Colloquium Details

Control and Logic

Abstract

We present control operators in the context of the Curry-Howard isomorphism. We start by analyzing the so called abortive control operators, e.g., callcc. The differing expressive power of various abortive control operators is captured in terms of their logical foundation. A new notion of logic, called minimal classical logic, is introduced. Minimal classical logic does not inforce the Ex Falso Quodlibet axiom. Computationally, this translates into operators which do not allow one to abort a program execution.

The class of control operators known as functional operators is shown to correspond to the abortive control operators plus a dynamically scoped variable, which characterizes the top-level. This class of operators provides a computational interpretation of subtractive logic. The benefit of a logic foundation is also shown by providing embeddings of well-known abstract machines into the logic itself.