Control reduction theories: the benefit of structural substitution

Abstract

Abstract The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a continuation. To the contrary, the control calculus, developed by the authors, distinguishes between jumps and terms . This alternative calculus, which derives from Parigot's λμ-calculus, works by direct structural substitution of evaluation contexts. We review and revisit the legacy theories of control and argue that provides an observationally equivalent but smoother theory. In an additional note contributed by Matthias Felleisen, we review the story of the birth of control calculi during the mid- to late-eighties at Indiana University.