= Typed lambda term
{title2=$\Gamma\vdash t:A$}
= Well-typed lambda term
{synonym}
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.
Back to article page
