Glossary

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 STELF. Some of these links point to extensive tutorials, but in those cases the first paragraph or two should include a definition of the concept.

• 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
• STELF signature
• Unification
• Uniqueness lemma
• Weakening lemma
• World checking
• World subsumption