Judgment
In the context of this wiki, we use the word judgment (or judgement) to refer to a relation that is defined inductively by a collection of inference rules. The judgments as types principle is a name for the methodology by which judgments are represented in LF.
A judgment in standard notation
For example, we can define a judgment that a natural number is even. The judgement holds when is even. It is inductively defined by the following inference rules:


Judgments as types
A judgment is represented in LF using the judgments as types methodology: we represent a judgment with an LF type, where the inhabitants of this type correspond exactly to derivations of the judgement.
For example, we represent the judgment using the following signature:
even : nat > type. evenz : even z. evens : {N:nat} even N > even (s (s N)).
The first declaration says that even is a family of types indexed by a nat. This means that for every term N : nat, there is a type even N. Note that the syntax > is overloaded: it is used to classify both typelevel families and termlevel functions. We then use this type family to define the types of two term constants.
The first term constant, evenz, has type even z. This constant represents the derivation that consists of the first inference rule above, which concludes .
The second term constant evens, corresponds to the second inference rule above, which, for any , constructs a derivation of from a derivation of . To encode this inference rule, the constant evens is given a dependent function type.
For example, the LF term
evens z evenz
represents the derivation
The term evens (s (s z)) (evens z evenz) represents a derivation that 4 is even, and so on.
See also
 Hypothetical judgements can be represented in LF in a higherorder manner, using LF binding to represent hypotheses.
 The introductions to Twelf discuss how judgments are represented in LF in more detail.
This page is incomplete. We should expand it.