Robert Harper
Tutorial on Mechanizing Metatheory with LF and Twelf

Do you want to learn how to use Twelf to specify, implement, and prove properties about programming languages? Come to the Twelf tutorial on January 19, 2009, co-located with POPL 2009, in Savannah, Georgia.

Learn to:

  • Represent languages and logics in LF
  • Prove metatheorems with Twelf
under the helpful guidance of Twelf experts. The tutorial will be a highly interactive introduction to LF and Twelf aimed at programming languages researchers. No prior experience with LF and Twelf is presumed. Participants will leave the workshop with experience in reading and writing LF representations of programming languages, and experience reading, writing, and debugging Twelf proofs.

The tutorial is organized and presented by the CMU Principles of Programming group. The presenters and TAs at POPL will be Dan Licata, William Lovas, Chris Martens, Rob Simmons, Bob Harper, and Karl Crary.