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.
- Most, but possibly not all, of the information from the Twelf homepage and the old Twelf Wiki that was the predecessor to this one is included on this wiki.
 External documentation
Besides information on this wiki and "official" documentation such as the User's Guide, 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 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 tutorial Type Theoretic Foundations of Programming Languages is intended for readers with little or no 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.