RIS ID
6939
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.
COinS
Publication Details
Bunder, M. (2003). Intersection type systems and logics related to the Meyer-Routley system B+. The Australasian Journal of Logic, 1 43-55.