[POPLmark] Re: [Provers] Re: adequacy

[Kevin Watkins]

On 5/5/05, Geoffrey A. Washburn <geoffw at cis.upenn.edu> wrote:
>         Benjamin tells me there is an article "How to believe a Twelf
>   proof" in development, which sounds like it will hopefully help others
>   understand what properties Twelf needs to verify.  However, based on the
>   title I kind of expect this is directed at readers of Twelf proofs, and
>   I think it would be valuable to develop a companion resource for those
>   trying to develop proofs.

If I were just starting to learn Twelf, I would focus on understanding
what a Twelf proof (total function) is, first, before trying to
understand Twelf's totality checker, or the messages it generates.

The best references I know of for understanding what a Twelf proof is
are Frank Pfenning's course notes for the course "Computation and
Deduction", especially Chapter 3, especially especially Section 3.7;
and the series of tech reports Frank has written over the years
describing several complex proofs (Church-Rosser, cut elimination,
etc.) in the Twelf style.

Once one learns to read and write such proofs, one becomes familiar
enough with the concepts and language to understand what Twelf's
totality checker is saying when it checks (or fails to check) them.

I posted links earlier to the tech reports I mentioned; also, all the
proofs from the tech reports come with the Twelf distribution, so one
has merely to peruse the examples/ directory to find pointers to the
TRs.

The course notes for Computation and Deduction are available at

  http://www.cs.cmu.edu/~fp/courses/comp-ded/handouts.html

As Karl mentioned, there is a twelf-users mailing list.  One can view
the list archives or join the list by visiting

  http://www.twelf.org/mailman/listinfo/twelf-list

There is also a Twelf Wiki.  At the moment there is not so much
information there, but there is a place for questions to be posted.

  http://fp.logosphere.cs.cmu.edu/twelf/

Kevin