Foundations of Functional Programming/Comparison of λ-calculi

This page compares λ-calculi according to various interesting properties they have. We give a table which concisely lays out all of the information for the calculi we discuss, followed by an explanation of each property featured in the table.

System	Implicit types?	Polymorphic types?	Type constructors?	Dependent types?	${\text{Type}}:{\text{Type}}$ property?	Turing complete?	Normalizing?	Consistent?	Type checking decidable?	Typability decidable?	Types unique?	Subject reduction theorem?
Untyped λ-calculus	Yes	No	No	No	No	Yes	No	No	Yes	Yes	Yes	Yes
Implicitly simply typed λ-calculus	Yes	No	No	No	No	No	Yes	Yes	Yes	Yes	No	Yes
Explicitly simply typed λ-calculus (λ→)	No	No	No	No	No	No	Yes	Yes	Yes	Yes	Yes	Yes
Implicitly typed second-order λ-calculus	Yes	Yes	No	No	No	No	Yes	Yes	No	No	No	Yes
Explicitly typed second-order λ-calculus (λ2)	No	Yes	No	No	No	No	Yes	Yes	Yes	Yes	Yes	Yes
Hindley-Milner type theory	Yes	Yes	No	No	No	Yes	No	No	Yes	Yes	No	Yes
λP	No	No	No	Yes	No	No	Yes	Yes	Yes	Yes	Yes	Yes
λP2	No	Yes	No	Yes	No	No	Yes	Yes	Yes	Yes	Yes	Yes
λω	No	No	Yes	No	No	No	Yes	Yes	Yes	Yes	Yes	Yes
λω	No	Yes	Yes	No	No	No	Yes	Yes	Yes	Yes	Yes	Yes
λPω	No	No	Yes	Yes	No	No	Yes	Yes	Yes	Yes	Yes	Yes
Calculus of constructions (λPω)	No	Yes	Yes	Yes	No	No	Yes	Yes	Yes	Yes	Yes	Yes
Naïve type theory (λ*)	No	Yes	Yes	Yes	Yes	?	No	No	No	No	Yes	Yes