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

[Yasuhiko Minamide]

> > [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

I wrote this code about 5 years ago. At that time, my strategy is to
formalize the CPS transformation as simple as possible.
So, I took a nominal approach. However, to simplify the treatment of
variable names, I gave some twists to the formalization.

> 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.  

I extracted the code of the verification of Plotkin's CPS transformation. 
You can find it at the following URL.

http://www.score.cs.tsukuba.ac.jp/~minamide/tmp/cps.tar.gz

The proofs in the code are closely based on the following paper.

 "Gordon Plotkin, Call-by-name, call-by-value, and the lambda-calculus,
  Theoretical Computer Science, 1975"

I added some comments in the code to clarify the correspondence and clean 
the code a little bit. Now, the code is 400 lines in length. 

>
> The proofs seem significantly more manual and hard to understand.  
>
As you noted, the proofs of the main lemmas are basically manual.
They closely correspond to the proofs of Plotkin and I think that
they are not difficult to understand.

>
> A pretty-printed HTML version with comments:
>	http://ltamer.sourceforge.net/coq/examples.CPS.html
>

I briefly checked the code above. I agree that the semantics preservation
proof is very simple. 

However, for the comparison, I would like to know what happens if 
recursive functions are added to the source language. 
The denotational semantics of the source language is based on the function 
space of Coq. It is not so clear how to extend the semantics for
recursive functions.

Yasuhiko Minamide