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

[Julien Narboux]

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

Hi,

I had a look at both versions. I also think it is very difficult to 
compare the two versions in terms of number of lines :

- Yours is LCF style to the extreme (with some fined tuned ltacs) and 
requires to know the behaviour of some library tactics (stricter_inster).
- Minamide's version seems to try to mimic the paper proof (for instance 
he derives an induction principle to have nice case names which reflect 
the distinction between terms which are values or not).

IMHO it is fair to say that yours is more automated, but I am not yet 
convinced it is easier to understand.

Regards,

Julien Narboux