[POPLmark] Experience report with Twelf

[nipkow@in.tum.de]

> What are people's experience with scaling in other settings
> (e.g., Coq, Isabelle, etc.)?  And how re-usable were the core
> proofs when extending a language?

I have found that proofs scale quite well in Isabelle, not just when adding
features but even when moving to a related language. Eg when moving from
(subsets of) Java to C++ we could reuse more than 50% of the proofs, even if
we needed to do lots of editing. Proofs written in Isabelle's structured
proof language scale even better.

Tobias