In the case of simply typed lambda calculus, a type has an inhabitant if and only if its corresponding proposition is a tautology of minimal implicative logic.
Similarly, a System F type has an inhabitant if and only if its corresponding proposition is a tautology of intuitionistic second-order logic.
Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence.
Richard Statman proved that for simply typed lambda calculus the type inhabitation problem is PSPACE-complete.
This programming language theory or type theory-related article is a stub.