[TYPES] Best pedagogical presentation of CPS?

[Paul Blain Levy]

Dear Benjamin,

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

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

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:

www.cs.bham.ac.uk/~pbl/mgsfastlam.pdf

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

Paul






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
>