Comparing models of the non-extensional typed λ-calculus

Abstract

In this paper we consider “powerset models” of the non-extensional typed lambda calculus. Although the interpretation of the type constructor ⇒ is in general not uniquely determined, we can make a canonical choice in this particular case; there exists a minimal interpretation of ⇒ (with respect to a certain class of interpretations) which yields models with a maximal theory (in that class).