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 June 10, 2013, 9:00-12:30, co-located with CADE 2013, in Lake Placid, New York. Location "Mirror Lake" in The Crowne Plaza Resort.
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 jointly presented by the the IT University of Copenhagen and the CMU Principles of Programming group. The presenters and TAs at CADE will be Taus Brock-Nannestad, Chris Martens, and Carsten Schürmann.
The tutorial will begin at 9:00AM. Get the slides!
- Part 1: Basic Twelf Skills
- Part 2: Mechanizing MinML
- Part 3: Combinators: Worlds and Adequacy
- Coda: What's next?
There will be a coffee break at 10:30AM.
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: see the download page.
- 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).