[Poplmark] Poplmark solution

[Karl Crary]

Dear All,

We've completed the challenge using Twelf, and we're attaching our 
solution.  This is a rough initial draft; we intend to put out a much 
more polished version in a few days.  The bulk of the credit for the 
here is due to our student Michael Ashley-Rollman, who implemented the 
formalizations and the proofs for this first draft.

The most difficult part of the challenge to implement in Twelf was part 
1a, the transitivity of algorithmic subtyping.  In particular, the proof 
of narrowing requires one to isolate the binding of interest, but doing 
so makes it difficult to deal with other bindings that may depend on 
it.  Fortunately, we were able to work around that difficulty.  Given 
that, it was easy to extend the proof to records, for part 1b.  Then, 
just for fun, we completed the algorithm's soundness and completeness 
proofs.

Part 2 is exactly the sort of the thing that Twelf was designed for, and 
it went through without any major obstacles.  We found it convenient to 
use a declarative formulation of subtyping, rather than the algorithmic 
formulation of part 1.  Finally, there was no additional code to provide 
for part 3.  Using Twelf's logic programming engine, the specification 
of the operational semantics may be used as an implementation; it's just 
a matter of inputting the appropriate query into Twelf.

It may be interesting to some of you how Michael came to do this.  For 
his undergraduate honors thesis, Michael is implementing the 
type-theoretic definition of Standard ML (from Harper & Stone, 2000) and 
proving its type safety in Twelf.  This left him well-positioned to 
tackle this challenge.  You should be hearing more about his work in the 
coming months.

Best,
Karl Crary and Robert Harper

-------------- next part --------------
A non-text attachment was scrubbed...
Name: poplmark.tgz
Type: application/x-compressed
Size: 22571 bytes
Desc: not available
Url : http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20050321/793f2222/poplmark-0001.bin