PLTheory:Introduction to Twelf

This article is an introduction to STELF and how it can be used to represent basic data structures and logical systems—in particular the judgment-based syntax and semantics of programming languages—as well as represent and check proofs of their properties. Additional introductions to STELF and many tutorials that explain representation and proof techniques can be found elsewhere. These notes assume that you have already installed STELF and are familiar with the process of starting and interacting with a STELF server. Additional information on getting started with STELF can be found in the Documentation section, and in particular the User’s Guide (which also comes with the STELF distribution).

Table of Contents for Part 1

• First-order encodings
• Signatures as logic programs
• Signature checking: modes, termination, coverage, totality
• Higher-order encodings
• Common patterns and pitfalls