Continuation models are universal for Xp-calculus
Martin O. Hofmann, Thomas Streicher · 1997
We show that a certain simple call-by-name cointinuation semantics of Parigot’s A, -calculus is cornplete. More precisely, for every A,-theory we coinstruct a Cartesian closed category such that the ensuing continuation-style interpretation of A,, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any &-category in the sense of is isomorphic to a continuation model [4] derived from a cartesiairlclosed category of continuations.