[TYPES] Best pedagogical presentation of CPS?
yuting at cs.umn.edu
Sat Feb 17 20:59:32 EST 2018
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:
On Wed, Feb 14, 2018 at 12:53 PM, Benjamin C. Pierce <bcpierce at cis.upenn.edu
> [ 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