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

[Adam Chlipala]

Yasuhiko Minamide wrote:
> 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.

I didn't mean to claim any particular negative characteristic of those 
proofs.  I think tactic-based proof scripts are simply doomed to be hard 
to understand in general.

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

It's not so bad to encode general recursion using co-inductive types for 
the denotations of expressions, but it is nowhere near as direct as the 
example I linked to earlier.  You're right that many language features 
don't fit very well into the approach I used there, and I think it's 
still an open problem whether it's possible to get around the barriers 
that appear in first attempts to adapt the technique.