[TYPES] Best pedagogical presentation of CPS?

[Philip Wadler]

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 <bcpierce at cis.upenn.edu>
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
>
>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20180215/2339545d/attachment.ksh>