[POPLmark] Experience report with Twelf

Greg Morrisett greg at eecs.harvard.edu
Fri Aug 19 10:30:11 EDT 2005


Stephanie Weirich wrote:
> This list has been a bit quiet lately, so I thought I'd get some
> discussion going again.

Thanks for cranking up the discussion again.  Matthew Fluet and
I have shared many of your frustrations in trying to formalize
some work on L-cubed and regions in Twelf.

One thing that we did find is that, although you end up writing
out a lot more in Twelf, it seems to scale well.  That is, we
started from a very little language, proved soundness for that,
and then started adding features, and relatively speaking, had
an easy time getting the proofs to go through.  It felt a lot
like programming in ML, where you add some new constructors to
a datatype, and the compiler tells you where you need to add
some new cases.  That is, the changes we had to make were largely
proportional to the complexity of the feature we were adding.
(Easy for me to say --- Matthew did all the hard work :-)).

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?

-Greg




More information about the Poplmark mailing list