POPL Tutorial
From The Twelf Project
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.
Register at the POPL 2009 registration site! The early registration deadline is December 19.
The tutorial is organized and presented by the CMU Principles of Programming group.
Schedule
- Session 1 (9AM-10AM): Overview of LF and Twelf
- Session 2 (10:30AM-12:30PM): Working with Twelf: LF constants, mode, %worlds, %total
- Session 3 (10:30AM-12:30PM): Adequacy
- Session 4 (1:30PM-3PM): Proving metatheorems: Type safety for MinML
- Session 5 (3:30PM-5PM): Break-out groups: choose one of several exercises (Church-Rosser, combinator logic, ...)
- Session 6 (5PM-5:30PM): What's next?
The tutorial will be based on a summer school course we ran this year, so you can browse those course materials if you want a better sense of what material we will cover.
Get Twelf before the tutorial!
The tutorial will be interactive, with participants writing Twelf code, so you should come with Twelf installed on your laptop.
Pre-built binaries of Twelf are available for most operating systems through the Twelf Night(ly).
Otherwise:
- you can build Twelf from the source tarball. You will need MLton or sml/nj.
- you can make yourself an account on the wiki, and do the exercises on your User:<login> page (linked at the top after you log in).
Then see Twelf with Emacs for the basics of interacting with Twelf. (You can also use Twelf without Emacs, by interacting with the Twelf server directly.)
