[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Wed, Feb 14, 2018 at 7:08 PM Benjamin C. Pierce <[email protected]> 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 > >
