From The Twelf Project
Learn Twelf on the wiki
- Read the introductions to Twelf first.
- The tutorials explain common Twelf tricks and techniques.
- The glossary defines Twelf terminology.
- The case studies present interesting applications of Twelf.
- Have a question? Ask Twelf Elf!
- The Twelf style guide discusses some best practices. There are also some suggested naming conventions.
- The Twelf User's Guide is the basic reference manual for Twelf.
- Active Twelf users should subscribe to the mailing lists.
- The LF bibliography lists research papers about LF and Twelf.
- Read about research projects using Twelf.
Besides information on this wiki, there have been a number of papers and tutorials explaining how to use Twelf for various purposes, as well as commentary on using Twelf.
- Andrew Appel's Hints on Proving Theorems in Twelf describes a particular methodology for using Twelf that is rather different than the strategy of proving metatheorems that predominates on this wiki (i.e. "the particular strange way they do it at Princeton").
- John Boyland's Using Twelf to Prove Type Theorems is a tutorial and experience report (he has also published a number of Twelf signatures).
- Dan Licata and Bob Harper have written a survey article called Mechanizing Metatheory in a Logical Framework. This paper provides a more formal introduction to the modern way of thinking about LF and Twelf than this wiki does.
- Alberto Momigliano's A Practical Approach to Co-induction in Twelf describes a technique for encoding Twelf-unfriendly co-inductive proofs as Twelf-friendly induction proofs (slides from a talk at TYPES 2006).
- Susmit Sarkar has notes from a mini-course, Mechanizing Metatheory in Twelf, at the University of Cambridge.
- John Altidor's Twelf Tutorial Report and Presentation are accessible without a strong background in programming language foundations.
Experience reports and commentary
- The POPLmark Challenge has a page on Twelf and commentary on the POPLmark submission from Carnegie Mellon that uses Twelf.
- Andrew Appel and Xavier Leroy's A list-machine benchmark for mechanized metatheory serves as both a tutorial and an experience report on using Twelf to prove theroems about compilers.