Introductions to Twelf
From The Twelf Project
The following introductory guides are available:
- Proving metatheorems with Twelf: if you have some background in programming languages but no prior experience with LF and Twelf, start with this introduction.
- POPL Tutorial 2009: course materials from a Twelf tutorial at POPL 2009. This path through the material is the best introduction to Twelf, but it may be harder to follow along with online than Proving metatheorems.
- Summer school 2008: notes from a Twelf course at the University of Oregon Summer School on Logic and Theorem Proving in Programming Languages, July 2008
- Twelf with Emacs: Using Twelf from within Emacs
- Twelf without Emacs: Running the twelf-server directly from the command line.
We plan to add other introductory articles for other audiences. If you have suggestions, please leave us a message.