[TYPES] Best pedagogical presentation of CPS?

[Xavier Leroy]

On Wed, Feb 14, 2018 at 7:08 PM Benjamin C. Pierce <bcpierce at cis.upenn.edu>
wrote:

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

 In my lectures I use Plotkin's original CBV presentation (the one that is
nicely compositional but produces lots of administrative redexes) and a
correctness proof based on big-step semantics that avoids the usual
difficulties with administrative redexes.  See
https://xavierleroy.org/mpri/2-4/, part 3, slides 65 to 71.

You can even mechanize the proof, it's a bit awkward in Coq but doable (see
part 6 for a naively-named solution, or my paper with Zaynah Dargaye
https://xavierleroy.org/bibrefs/Dargaye-Leroy-CPS.html for a de Bruijn
solution).

For a proof using small-step semantics, I'd rather use Danvy and Nielsen's
transformation (which avoids generating administrative redexes) than work
through Plotkin's original proof with the colon translation.

Finally, for a higher-level presentation you could go straight to monads
and use Moggi's computational lambda-calculus to reason about the semantics
of monadic terms.

Hope this helps,

- Xavier Leroy


> Many thanks,
>
>     - Benjamin
>
>