Re: [TYPES] Best pedagogical presentation of CPS?
Adam Chlipala <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] 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).