Abstract

Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple (→) types to intersection (or →∧) types allows all closed lambda terms to have types. The corresponding →∧ logic, related to the Meyer–Routley minimal logic B+ (without ∨), is weaker than the →∧ fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the →∧ logics that correspond to certain interesting subsystems of the full →∧ type theory.