The types of the simply typed lambda calculus are constructed from base types (or type variables) and given types σ,τ we can construct . Church used only two base types o for the type of propositions and ι for the type of individuals. Frequently the calculus with only one base type, usually o, is considered.
associates to the right: we read as . To each type σ we assign a ...
To define the set of well typed lambda terms of a given type, we introduce typing contexts which are sequences of typing assumptions of the form x:σ where x is a variable. We introduce the judgment which means that t is a term of type σ in context Γ which is given by the following typing rules:
Examples of closed terms are:
(I),
(K), and
(S).
These are the typed lambda calculus represen ...
