[POPLmark] Meta-comment

[Frank Pfenning]

> FWIW, I meant "do" as in me doing the gruntwork with the tool watching over
> my shoulder, not "avoid" as in the tool doing it all by itself.  I'm not
> that naive... :-)

Actually, the step from a good tool to a mostly automatic tool is
smaller than you might imagine.  Carsten Schuermann and I had a paper in
CADE-15 (1998) on automated deduction for meta-theory that was later
elaborated on in his Ph.D. thesis (2000).

Among the successes:

 - Automatic proof of the admissibility of cut for classical and intuitionistic
 logic with a reasonably rich set of connectives.  You only state
 the theorem and the induction order; the rest is automatic.

 - Automatic proof of each lemma in the Church-Rosser theorem for the
 untyped lambda-calculus following the Tait/Martin-Loef method of
 parallel reduction.  You only state each lemma and the induction
 order; the rest is automatic.  If I recall correctly, the
 simply-typed lambda-calculus also works.

 - Automatic proofs of several progress and preservation properties
 for small functional languages.  I don't recall the high watermark
 in terms of complexity of language features.

Unfortunately, the meta-theorem prover is now obsolete in the sense that
it currently produces no checkable certificates and has not been updated
for some time.  I believe Carsten's plan is to resurrect this once
the Delphin language has been released.

  - Frank
----------------------------------------------------------------------
Carsten Schurmann.
Automating the Meta-Theory of Deductive Systems,
Department of Computer Science, Carnegie Mellon University, August 2000.
Available as Technical Report CMU-CS-00-146.
<http://cs-www.cs.yale.edu/homes/carsten/papers/S00b.ps.gz>

Carsten Schurmann and Frank Pfenning. Automated theorem proving in a
simple meta-logic for LF. In Claude Kirchner and Helene Kirchner,
editors, Proceedings of the 15th International Conference on Automated
Deduction (CADE-15), pages 286-300, Lindau, Germany, July
1998. Springer-Verlag LNCS 1421.
<http://www.cs.cmu.edu/~fp/papers/cade98m2.pdf>