Glossary

From The Twelf Project

This glossary should include most of the unfamiliar concepts that someone with an undergraduate-level understanding of type theory would encounter in the process of learning to use Twelf. Some of these links point to extensive tutorials, but in those cases the first paragraph or two should include a definition of the concept.

Feel free to add new glossary entries to the list below. If you encounter a piece of terminology or jargon you haven't seen and it isn't here already, or if a link doesn't answer your question, let us know on the talk page.

Twelf keywords

---

%. %abbrev %assert %block %clause %covers %define %deterministic %establish %freeze %infix %prefix %postfix %mode %name %prove %query %querytabled %reduces %solve %subord %tabled %terminates %thaw %theorem %total %trustme %unique %use %worlds

• Adequacy
• Alpha-equivalence (i.e. "α-equivalence")
• Beta-equivalence (i.e. "β-equivalence")
• Canonical form
• Canonical forms lemma
• Compatibility lemma
• Congruence relation
• Congruence lemma
• Constraint domain
• Coverage checking
• Effectiveness lemma
• Equality
• Equivalence relation
• Eta-equivalence (i.e. "η-equivalence")
• Eta-long form (i.e. "η-long form")
• Exchange lemma
• Explicit parameter
• Explicit context
• Extrinsic encoding
• Function
• Ground
• Higher-order abstract syntax
• Higher-order judgement
• Hereditary substitution
• Hypothetical judgment
• Implicit parameter
• Intrinsic encoding
• Judgment
• Judgments as types
• LF
• Logic programming
• Meta-logic
• Metatheorem
• Mode checking
• Object logic
• Relation
• Regular worlds
• Respects lemma
• Substitution lemma
• Subordination
• Tabled logic programming
• Tactical theorem proving
• Theorem prover
• Totality assertion
• Totality checking
• Type family
• Twelf signature
• Unification
• Uniqueness lemma
• Weakening lemma
• World checking
• World subsumption