[POPLmark] Comparison of certified code transformations for functional languages?

[Adam Chlipala]

Xavier Leroy wrote:
> Here are two other examples of mechanized proofs of semantics preservation
> for CPS translations:
>   

Thanks!

> [1] "Verifying CPS Transformations in Isabelle/HOL"
>     Yasuhiko Minamide Koji Okuma
>     http://www.score.is.tsukuba.ac.jp/~minamide/papers/merlin03.pdf
>   

I found this code online at
    http://www.score.is.tsukuba.ac.jp/~minamide/verification.html

It looks like the development is at least twice as long as mine 
lines-of-code wise, at 632 vs. 238.  I wasn't sure at a glance how to 
calculate a fair backwards slice of required developments, so I counted 
Lt.thy and Plotkin.thy.  It uses a smaller (and untyped, as far as I can 
tell) source language, omitting a base type and products.  The proofs 
seem significantly more manual and hard to understand.  Perhaps an 
Isabelle expert could tell me if I'm just being unfair here. :-)

> [2] "Mechanically verifying correctness of CPS compilation"
>     Ye Henry Tian 	
>     http://crpit.com/confpapers/CRPITV51Tian.pdf
>   

This code is online at:
    http://www.cs.mcgill.ca/~ytian8/CPS/

I counted the size of all files but 
[cps-complete|cps-sound2|cps-sound3|cps-uniqueness].elf, which don't 
seem directly related to the tasks I was interested in, and came up with 
307 lines.

I didn't notice anything that looked like a type preservation proof for 
the CPS translation.  Can anyone else spot one?

A basic design decision of the CPS translation here puzzled me, so 
here's a question for the Twelf wizards about what limitations that 
decision creates.

The CPS translation is typed as:
cpsExp : exp -> (cval -> cexp) -> cexp -> type.

The rule for function abstraction goes like:
cpsExp (lam E) K (K (lam+ E'))
       <- % more stuff....

The thing that catches my eye is that the continuation is simply 
applied, without using one of the constants representing the syntax of 
the target language.  How does a representation choice like this impact 
the implementation of later compiler phases that need to do things like 
calculate sets of free variables, which could include continuation 
variables?  (For instance, closure conversion)

This question is related to my vague feeling that something seems too 
easy about this formalization. ;)  Looking at the syntax of the target 
language in cps.elf, I'm surprised to find that function application 
looks almost the same as projection from a pair.  This doesn't mesh with 
my informal idea that a CPS transform is rearranging function-call 
control flow in some interesting way, while code that just manipulates 
pairs is simply linearized locally.

> - Closure conversion.  Proving semantics preservation in an untyped
>   setting is not really hard, but in a typed setting you need
>   existential types in the target language.
>   

My implementation of certified, statically-typed closure conversion 
avoids existential types by including monolithic "closed code" and "open 
code" types:
    http://ltamer.sourceforge.net/coq/CTPC.CC.html