[POPLmark] [Provers] Re: Adequacy for LF

[Greg Morrisett]

Benjamin Pierce wrote:
> By contrast, what we've seen of Twelf is extremely
> attractive in many ways -- many things seem to work impressively smoothly --
> but the technology is much fancier and it's hard to get a sense of whether
> it can be used (either "in principle" or "right now") to carry out the full
> range of activities that we PL as folks are used to doing with our pencils

Just to clarify -- it's possible to code up deBruijn representations
in LF/Twelf as well.  I think the real question is if you commit to
using HOAS, where does it really bite?  Possible answers so far:

* if your notion of substitution is non-standard
* if you need to get your hands on the context

Perhaps there are others?

I'm also curious about the evolutionary path.  It's clear that we're
going to want to mod out by more than alpha-equivalence for many
things, and I don't yet see how this will be handled nicely in
*any* system.

For instance, I still find modeling an abstract machine with a heap,
which I want to consider as a partial map from (alpha-varying) labels
to values (which may have free occurrences of those labels), to be
very awkward to encode.  deBruijn representation blows here, because
I don't want the order of the bindings to matter.  But I haven't
found a nice way to do this in Twelf either...  [Karl, Bob,
attack mode off.  I didn't say "It can't be done."  I very
politely said that "I haven't found a nice way to do this."]

I've been disappointed by the apparent lack of "polymorphism"
in Twelf -- I seem to have to define various kinds of lists at
every level.  For someone used to coding instead of proving,
that's painful.  Is there a way around this?

And finally, I find it somewhat annoying that when
I write a simple, total function, I have to step out to the
meta-level to establish that it is indeed a function.
Maybe there's a good way around this too?

-Greg

p.s. Most fun reading I've had in a while...