[TYPES] Best pedagogical presentation of CPS?

Yuting Wang yuting at cs.umn.edu
Sat Feb 17 20:59:32 EST 2018

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

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:


Best Regards,
- 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

More information about the Types-list mailing list