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

[Kevin Watkins]

On 5/4/05, Peter Sewell <Peter.Sewell at cl.cam.ac.uk> wrote:
> I wouldn't suggest anyone should - in this context it's simply an
> example of a more intricate dynamic semantics than that of SML, and
> one for which the natural pen-and-paper semantics requires computation
> under binding contexts.  I would like to know decent formalisation
> strategies for those (and they might well vary depending on the choice
> of HOAS/De Bruijn/Nominal sets/...)

There are some instances of this kind of reasoning in HOAS style in
the examples that come with the Twelf distribution.  One is the proof
of the Church-Rosser theorem for the untyped lambda-calculus, in the
examples/church-rosser directory.  The proof is essentially the one
used by Tait and Martin-Lof, and relies on relating two notions of
reduction, both of which involve reduction under abstractions.  The
proof is described in a TR:

  Frank Pfenning, "A proof of the Church-Rosser theorem and its
representation in a logical framework", Tech Rpt CMU-CS-92-186, Sept.
1992.

  http://www.cs.cmu.edu/~fp/papers/cr92.ps

The other is the proof of cut elimination for intuitionistic and
classical first-order logics in the examples/cut-elim directory.  The
cut elimination procedure can be viewed as a "natural" or "big-step"
operational semantics for proofs.  The cut elimination procedure
obviously needs to normalize proofs underneath binders.  The proof is
described in another TR:

  Frank Pfenning, "A structural proof of cut elimination and its
representation in a logical framework", Tech Rpt CMU-CS-94-218, Nov.
1994.

  http://www.cs.cmu.edu/~fp/papers/cutelim94.ps

Also, I should have given a URL to the report on the inverse CPS
transform I mentioned before as an example of reasoning intensionally
with variable occurrences.  It's available at

  http://www.cs.cmu.edu/~fp/papers/cpsocc95.ps

I should say that some of these examples are from much earlier
versions of Elf/Twelf, and so, although they run fine in the latest
Twelf distributions, they don't show off all the latest features.  But
in any case, they give the flavor of how one reasons with binders in
the HOAS style in Twelf.

Kevin