*Semantics Club 09 03 2001*

# On the CPS transformation from the computational lambda calculus to the linear lambda calculus

### Abstract

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).