From The Twelf Project
Jump to: navigation, search
If you are not already familiar with Twelf, you should read the introductions to Twelf before reading the tutorials on this page. See the documentation page for other resources.

Types of tutorials:

Feel free to write new tutorials and add them to this page.

These tutorials are also gathered in the tutorial category.

Proof techniques



  • Strengthening - how to convince Twelf that a term does not depend on some assumptions.
  • Explicit termination metrics - how to use a termination metric other than the subderivation ordering.
  • Simplifying dynamic clauses - how to streamline certain proofs about relations that introduce hypotheses.
  • Canonical forms lemma for a progress theorem - how to get this lemma for free when you can, and how to prove it explicitly using equality when you can't.
  • Structural properties of a hypothetical judgement - how to get structural properties for free when you can, and how to prove them explicitly when you can't.
  • Evaluation contexts - how to represent evaluation contexts as LF functions
  • User-defined constraint domains - how to make encodings more intrinsic by replacing predicates with indexing, and how to use Church-encodings to create special index types that are similar to constraint domains in that they admit non-trivial equations on their elements.

For larger examples of Twelf in action, see see the case studies.