Josh Berdine (partly joint with Peter O'Hearn, Uday Reddy, and Hayo Thielecke)
Carnegie Mellon University

Control Contexts versus Continuations in Linearly Typed CPS

In this talk I will:
-give an overview of some motivations behind our work on linear and affine type systems for continuation-passing style (CPS),
-give an introduction to the basic ideas, and
-focus on one of the semantic issues we ran into: the distinction between "control contexts" and "continuations".

The overall aim of this work is to constrain, or reduce the expressiveness of, the CPS language using a linear type system. In the simplest cast of the target of the CPS transform of lambda-calculus, this restriction is accomplished by forcing the current continuation to be used linearly. However, for other source languages, limiting the use of continuations--destinations of jumps with arguments--is not sufficient. Instead, the parameter(s) of the semantics which encode "the meaning of the rest of the computation", which we term the control context, must be identified and its use restricted. As evidence that this distinction is necessary, we give an interpretation of call/cc and abort which uses continuations linearly but control context nonlinearly.

Host: John Reynolds
Appointments: Jennifer Landefeld

Principles of Programming Seminars