[TYPES] Best pedagogical presentation of CPS?

[Adam Chlipala]

On 02/14/2018 12:53 PM, Benjamin C. Pierce 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)?

I'm not too well-informed about all the different varieties of CPS 
transform, but one for simply typed lambda calculus from my Lambda Tamer 
library <http://ltamer.sf.net/> might qualified as appealingly 
pedagogical.  It takes up a bit over 100 lines of Coq source code, 
including defining the transform and proving its correctness.  The 
semantics is a tagless interpreter, which greatly simplifies things vs. 
operational semantics.

Unfortunately, I did this project in the days before GitHub, and its 
SourceForge-hosted web page seems to be offline just now!  But here's a 
temporary link to the file in question 
<http://people.csail.mit.edu/adamc/tmp/CPSify.v> (found in 
examples/STLC/CPSify.v in the full distribution).