[POPLmark] Comparison of certified code transformations for functional languages?
adamc at cs.berkeley.edu
Tue May 8 16:40:32 EDT 2007
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.
More information about the Poplmark