[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected] > 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 <[email protected]> University of Minnesota, Dept. of Computer Science http://www.cs.umn.edu/~yuting
