[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Amr Sabry and I were the first to show that CPS is sound and complete with a reduction semantics. Sabry and Felleisen had previously shown a translation sound and complete with equational semantics. A reflection on call-by-value Amr Sabry and Philip Wadler. ACM Transactions on Programming Langaguage, 19(6):916-941, November 1997. http://homepages.inf.ed.ac.uk/wadler/papers/reflection- journal/reflection-journal.pdf https://dl.acm.org/citation.cfm?doid=267959.269968 The results are, to my mind, surprisingly straightforward, with the tricky part being to get the source and target calculi and the administrative reductions correct. Plotkin showed soundness but not completeness. When I presented these results at Edinburgh (long before I moved there), Plotkin was in the audience. With some trepidation, I said, "I believe this improves on your result of twenty years ago." Gordon immediately responded, "Yes, but you've had twenty years!" Cheers, -- P . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ On 14 February 2018 at 15:53, Benjamin C. Pierce <[email protected]> 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 > >
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
