[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Daniel C. Wang]

Dan Licata wrote:
> On Jun01, Daniel C. Wang wrote:
>   
>> 1. There isn't a nice "nat" library I could just include.
>>     
>
> What we have works okay---I've used parts of the nat "library" from this
> task in several other projects, for example.  There are definitely
> issues of namespace management and parametrization and reuse (not as
> much for nat, but for other types), though.  To that end, we're working
> on a module system for Twelf this summer, so check back in September.
>
>   
This will be a big improvement!
>> By the adequacy of the encoding of the informal presentation into my LF
>> signature, the theorem statement in question is equivalent to the following:
{stuff deleted}
>  Bob and I attempted to explain
> these details in the Mechanizing Language Definitions draft that I've
> mentioned; it's linked from my Web page.  I'd be happy to explain these
> issues further if anyone has questions!
>   
The adequacy theorem you presented in the draft is far from non-trivial. 
I'd personally, would like to see it mechanized in Twelf.  The informal 
presentation of the proof in the paper seems to take unfair liberties 
with the treatment of alpha-equality and substitution. In fact every 
adequacy theorem I've seen of this sort seems to take the same liberties.

It would be nice to see a mechanized treatment of adequacy that shows 
the higher-order encoding is one-to-one with a standard nameless or 
nominal 1st order-encodings. This I understand is a non-trivial request 
but it would be quite ironic if you cannot formalize in Twelf the 
adequacy theorems for which Twelf depends on. It occurs to me that there 
are several ways to state such a theorem in Twelf, some approaches use 
HOAS others are completely first order. I'm not sure which is the most 
interesting one to do.

I guess this suggests an interesting Poplmark Grand Challenge(TM). That 
is to formalize all the meta-theory that makes Twelf work. Such a proof 
is clearly of interest because Twelf is of interest and it's really 
non-trivial.  However, it might be very mind-bending to understand the 
Twelf solution to this Grand Challenge. Then again compilers bootstrap 
themselves all the time now. Why shouldn't my verification system verify 
itself. Okay, my head hurts from thinking about that...