[Provers] Re: [POPLmark] Submissions page and comments updated

[Jerome Vouillon]

On Thu, Apr 28, 2005 at 10:38:56PM -0400, Benjamin Pierce wrote:
> I completely agree with Frank's points and concur that the best way
> to prove something in a formal setting may be different from what is
> natural for a paper proof.

I believe that, in this case, the formulation of the evaluation
adopted in the Twelf proof (and in my Coq proof) is also the most
natural for a paper proof.  There are currently two issues with
the paper proof that hint at this (beside the fact that the proof
of lemma A.18 is only sketched).

First, for the proof of lemma A.18, you write:
   In each case, we consider the last rule used in the derivation of
   G |- E[t] : T and apply the induction hypothesis.
But the induction hypothesis cannot be applied when the last rule is
the rule T-Sub.

Second, the following sentence from the proof of the Preservation
theorem is confusing, as it is not used at all.
    By Lemma A.18, G |- t0 : T0 for some T0.

-- Jerome