[POPLmark] Adequacy for LF

[Stephan Zdancewic]

Karl Crary wrote:

> There's been some confusion about the adequacy of our encoding of the 
> operational semantics; in particular, why our encoding is adequate, 
> given that the paper presents the semantics using evaluation contexts 
> and our encoding does not.  We wanted to clarify why it is adequate, 
> and moreover, why we thought its adequacy was obvious.

Hi Karl,
  I would also like to elaborate a bit more on why we originally gave 
the Twelf implementation a grade of "-" with respect to the operational 
semantics.  Part of the confusion (and this is probably our fault 
entirely) is that the point of PoplMark is *not* to prove the soundness 
of FSub.  Instead, the point is to allow us to compare proofs of "the 
same thing" using different theorem proving and term representation 
strategies.  Because different term representations will likely need to 
use different proof techniques, there has to be some wiggle room for 
what exactly "the same thing" is, but by trying to keep as many features 
of the formalism the same across different implementations, we had hoped 
to make comparison easier.  In addition, the other point of the PoplMark 
Challenge is to see how the technologies scale to handle different 
language constructs, including things like exceptions, etc. that are 
more cleanly handled by evaluation contexts.  (See Peter's mail.)
 
  As you rightly point out, the operational semantics for FSub doesn't 
require evaluation contexts and omitting them may make the proofs 
cleaner.  In fact, never have we said that your solution was inadequate 
(in the technical sense).  Our objection was solely to the fact that it 
didn't follow the spirit of the challenge.  We should have clarified 
this from the beginning.

  Putting the adequacy of your original encoding aside for the moment, 
let me ask you this: How hard would it be to formalize the operational 
semantics, using evaluation contexts, following the paper version as 
closely as possible?  My impression is that it wouldn't be that much 
harder than the existing solution.  If it *would* be significantly 
harder, then that in itself is interesting, and I would like to 
understand why. 

Thanks,
  Steve