Completeness of continuation models for

Synopsis We show that a certain simple call-by-name continuation semantics of Parigot's *_-calculus is complete. More precisely, for every *_-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of *_, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any *_-category in the sense of [8] is isomorphic to a continuation model [6] derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of * _ developed by Ong and Stewart [7]. 1 Introduction and Summary Parigot's *_-calculus [9] is a proof term assignment system for propositional classical logic and can at the same time be considered as a prototype for a functional programming language incorporating explicit handling of continuations. The original motivation for this calculus was to give a functional interpretation for proofs in classical AF2--a certain system of second-order arithmetic [5]