Semantics Club 09 03 2001
Though the call-by-value continuation-passing style (CPS) transformation from the computational lambda calculus into the simply typed lambda calculus has been shown to be equationally sound and complete (Sabry and Felleisen, 1992), it is not full: there are inhabitants of the interpreted types which are not in the image of the transformation. There are at least two ways to obtain full completeness for the transformation: either (1) by enriching the source calculus with first-class continuations, or (2) by restricting the target calculus using some typing discipline. The first one is standard. In this talk I sketch how the second approach can be carried out along the line of recent work on "linearly used continuations" by Berdine, O'Hearn, Reddy and Thielecke (CW'01). The basic idea is surprisingly simple (and old): since a continuation is used precisely once (provided there is no controls), we can replace the interpretation (Y->R)->(X->R) of a function type X->Y by (Y->R)-o(X->R) using the linear function type "-o" - and it does work. With some considerations on the underlying semantic structures, I put the CPS transformation in the general context of monadic transformations into a linear lambda calculus (fragment of DILL of Barber and Plotkin). Regrettably, the proof I have now is heavily syntactic, but I expect that a semantic proof will be available, by appealing to some model construction techniques (e.g. categorical glueing).