Documentation out of dateLearn more
Introductions to Twelf
Recommended
Section titled “Recommended”- Our recommended introduction to STELF is Proving metatheorems with STELF. If you have some background in programming languages but no prior experience with LF and STELF, then Proving metatheorems is probably right for you!
Other tutorials
Section titled “Other tutorials”- Andrew Appel’s Hints on Proving Theorems in STELF describes a particular methodology for using STELF that is rather different than the strategy of proving metatheorems that predominates on this wiki (also known as “the particular strange way they do it at Princeton”).
- John Boyland’s Using STELF to Prove Type Theorems is a tutorial and experience report.
- 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 STELF than this site does.
- Alberto Momigliano’s A Practical Approach to Co-induction in STELF describes a technique for encoding STELF-unfriendly co-inductive proofs as STELF-friendly induction proofs (slides from a talk at TYPES 2006).
- John Altidor’s tutorial and slides are accessible to folks without a strong background in programming language foundations.
Experience reports and commentary
Section titled “Experience reports and commentary”- The POPLmark Challenge has commentary on the POPLmark submission from Carnegie Mellon that uses STELF.
- Andrew Appel and Xavier Leroy’s A list-machine benchmark for mechanized metatheory serves as both a tutorial and an experience report on using STELF to prove theroems about compilers.
Curriculum from past STELF tutorials
Section titled “Curriculum from past STELF tutorials”- POPL Tutorial 2009: course materials from a STELF tutorial at POPL 2009. This path through the material is the best introduction to STELF, but it may be harder to follow along with online than Proving metatheorems.
- Summer school 2008: notes from a STELF course at University of Oregon Summer School on Logic and Theorem Proving in Programming Languages, July 2008.
STELF user’s guide
Section titled “STELF user’s guide”The STELF User’s Guide was the basic reference manual for STELF prior to the STELF Wiki, and is still the authoritative source for some topics.