Home

Reasoning with Continuations II: Full Abstraction for Models of Control


Author(s) : Matthias Felleisen Dorai Sitaram, 
Publisher : N/A
Publication Date : 1990
ISSN : N/A
Abstract : A fully abstract model of a programming language assigns the same meaning to two terms if and only if they have the same operational behavior. Such models are well-known for functional languages but little is known about extended functional languages with sophisticated control structures. We show that a direct model with error values and the conventional continuation model are adequate for functional languages augmented with first- and higher-order control facilities, respectively. Furthermore, both models become fully abstract on adding a control delimiter and a parallel conditional to the programming languages. 1 The Control Structure of Lisp Many programming languages, in particular Lisp [17, 24] and Scheme [22, 26], contain sophisticated control structures with constructs for labeling the control state at an arbitrary point for later reuse. Since Lisp is an expression-oriented language, a jump to a labeled control state---just like a procedure---may also pass a parameter so that it is possible to communicate results between control points. In most Lisp systems, control points have a special status, distinct from all other values. The The work of both authors was partially supported by,