Linear Continuations

Abstract

We present a functional interpretation of classical linear logic based on the concept of linear continuations. Unlike their non-linear counterparts, such continuations lead to a model of control that does not inherently impose any particular evaluation strategy. Instead, such additional structure is expressed by admitting closely controlled copying and discarding of continuations. We also emphasize the importance of classicality in obtaining computationally appealing categorical models of linear logic and propose a simple “coreflective subcategory” interpretation of the modality “!”.