[TYPES] Best pedagogical presentation of CPS?

Paul Blain Levy P.B.Levy at cs.bham.ac.uk
Thu Feb 15 14:10:34 EST 2018

Dear Benjamin,

This probably doesn't answer your question, but...

In my view, the call-by-value CPS transform is a composite of three

1. From call-by-value lambda-calculus to fine-grain call-by-value.

2. From fine-grain call-by-value to call-by-push-value.

3. From call-by-push-value to a special fragment of lambda-calculus,
where nothing returns. (I like to call it "Calculus of no return".)

Part (3) is in my view the "real" CPS transform.  Part (1) and (2) are
about general effects.

The part which involves fiddling (administrative redexes) is (1). 
That's because (coarse-grain) call-by-value doesn't distinguish between
values and computations, so when it sees a value that's a tuple of
tuples of tuples (say), it won't realize that it's a value and will
reevaluate it.

Correctness of (2) and (3) is immediate if you use a CK-machine
(computation+stack) to present operational semantics.  Agreement of
CK-machine and big-step is also easy.

This is in my book (and thesis, for an older version).  For a more
recent but brief story, here are the slides from my course on
lambda-calculus, effects and call-by-push-value at Midlands Graduate
School 2017:


The last part ("Control") is about CPS, but it only gives the outline,
so it doesn't show the translation on terms.


On 14/02/18 17:53, Benjamin C. Pierce wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Dear Types types,
> What is the best presentation of the continuation-passing transform and its proof of correctness (“best” in the sense of clarity of both algorithm and proof, not efficiency or generality)?
> Many thanks,
>     - Benjamin

More information about the Types-list mailing list