PLTheory:Introduction to Twelf

From The Twelf Project
Jump to: navigation, search

This article is an introduction to Twelf 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 Twelf and many tutorials that explain representation and proof techniques can be found elsewhere. These notes assume that you have already installed Twelf and are familiar with the process of starting and interacting with a Twelf server. Additional information on getting started with Twelf can be found in the Documentation section, and in particular the User's Guide (which also comes with the Twelf distribution).

Table of Contents for Part 1

  1. First-order encodings
  2. Signatures as logic programs
  3. Signature checking: modes, termination, coverage, totality
  4. Higher-order encodings
  5. Common patterns and pitfalls