History

Please fill in your query. A complete syntax description you will find on the General Help page.
Inhabitation of types in the simply typed lambda calculus. (English)
Inf. Comput. 119, No.1, 14-17 (1995).
Summary: In the 1960s, mathematicians from Eastern Europe showed that every admissible rule in the intuitionistic implicational calculus is derivable. We prove the corresponding proposition for the simply typed lambda calculus: The type $μ_1 \to μ_2 \to \cdots μ_m \to v$ is inhabited iff for each substitution $s$ of types for the variables in $μ_1, \dots, μ_m$, $v$ the inhabitation of $s (μ_1), \dots, s(μ_m)$ implies the inhabitation of $s(v)$.