[TYPES] Best pedagogical presentation of CPS?

[Yuting Wang]

Dear Benjamin,

As part of my thesis work, I have went through the exercise of formalizing
the CPS transformation in the style of Danvy & Filinski for simply typed
lambda terms. Both the specification and the correctness proofs of the
transformation exploit a form of higher-order abstract syntax, which leads
to very concise code and proofs. For example, the essential part of the
specification is given as follows:

cps (nat N) K (K (nat N)).
cps (abs R) K (K (abs k\ abs x\ R' k x)) :-
  pi k\ pi x\ (pi k'\ cps x k' (k' x)) => cps (R x) (y\ app k y) (R' k x).
cps (app M1 M2) K M' :-
  pi x1\ cps M2 (x2\ app (app x1 (abs K)) x2) (M2' x1),
  cps M1 M2' M'.

It is basically a direct translation of Figure 2 in Danvy & Filinski's
paper(https://doi.org/10.1017/S0960129500001535), albeit in a relational
style.

You can find the full source code at http://www.cs.yale.edu/homes/wang-
yuting/cps/. The dynamic semantics of the language is given in a small-step
style. The proof of semantics preservation is based on a logical relation.

You can also find a more complete story on formalizing transformations on
functional programs using our HOAS-based approach via the following link:

   http://sparrow.cs.umn.edu/compilation


Best Regards,
- Yuting
http://www.cs.yale.edu/homes/wang-yuting/

On Wed, Feb 14, 2018 at 12:53 PM, 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
>
>


-- 
Yuting Wang <yuting at cs.umn.edu>
University of Minnesota, Dept. of Computer Science
http://www.cs.umn.edu/~yuting