Mechanizing Metatheory in Twelf

A tutorial course

This is the course web page for a theory minicourse on Twelf. The course abstract is here.

Here are instructions on getting and compiling Twelf.

The lecture schedule is as follows:

• Lecture 1, Tue 27 Feb, 2007, 10.00 - 12.00, FW11 (notes in pdf, ps)
• Lecture 2, Thu 1 Mar, 2007, 10.00 - 12.00, FW11 (notes in pdf, ps)
• Lecture 3, Mon 5 Mar, 2007, 10.00 - 12.00, FW11 (notes in pdf, ps)

The course is loosely based on a variety of examples and documents used over the years to learn about Twelf. Here are a few documents that explain the art of writing proofs in Twelf:

• Mechanizing Metatheory in a Logical Framework, Robert Harper and Daniel Licata, October 2006.
• How To Believe a Twelf Proof, Robert Harper and Karl Crary, unpublished note.
• The Twelf User's Guide, version 1.4, Frank Pfenning and Carsten Schurmann.