Typed lambda term ($\Gamma ⊢t:A$)

A typed lambda term carries a type derivation under a context of typed free variables. The rules for variables, abstraction, and application correspond to assumptions, the implication introduction rule, and the implication elimination rule under the Implicational Curry-Howard correspondence. General fixed-point combinators belong to the untyped lambda calculus; self-application cannot be given a finite simple type.