Re: [TYPES] Best pedagogical presentation of CPS?

François Pottier <[email protected]>
Newsgroups gmane.comp.science.types
Message-ID <[email protected]>
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


Dear Benli,

Le 14/02/2018 à 18:53, Benjamin C. Pierce a écrit :
> What is the best presentation of the continuation-passing transform and its proof of correctness?

I recently taught CPS and its proof of correctness, formulated
in a small-step style. Despite the huge literature on CPS I had
some surprises and wrote down some of my findings in this paper
(in submission):

   http://gallium.inria.fr/~fpottier/publis/fpottier-cps.pdf

The paper is still more complicated than I would like. I am
thinking that perhaps the "small-step simulation diagram"
approach is too complex, and a proof based on a big-step
operational semantics would be simpler. Investigating this
is on my TODO list for next year.

The slides of my lecture on CPS are here:

 
https://gitlab.inria.fr/fpottier/mpri-2.4-public/blob/master/slides/fpottier-04.pdf

I hope this is useful. Your comments are welcome!

-- 
François Pottier
[email protected]
http://gallium.inria.fr/~fpottier/
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.