Documentation
From The Twelf Project
Contents |
[edit] 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.
[edit] Reference
- 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.
[edit] 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.
[edit] Tutorials
- 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.
[edit] 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.
[edit] Other
Is there some form of documentation that should be on this wiki but isn't? Add it to The Twelf Project:To do list or contribute it.
