A formulae-as-type notion of control

Publisher Website
Google Scholar
Abstract
The programming language Scheme contains the con- trol construct call/cc that allows access to the cur- rent continuation (the current control context). This, in effect, provides Scheme with first-class labels and jumps. We show that the well-known formulae-as- types correspondence, which relates a constructive proof of a formula a to a program of type (Y, can be extended to a typed Idealized Scheme. What is surprising about this correspondence is that it relates classical proofs to typed programs. The existence of computationally interesting "classical programs" - programs of type (Y, where Q holds classically, but not constructively - is illustrated by the definition of conjunctive, disjunctive, and existential types us- ing standard classical definitions. We also prove that all evaluations of typed terms in Idealized Scheme are finite.

This publication has 0 references indexed in Scilit: