Polymorphism is not set-theoretic
John C. Reynolds
Discussion led by Fran Mota on November 19, 2014
Abstract:
PDFThe polymorphic, or second-order, typed lambda calculus is an extension of the typed lambda calculus in which polymorphic functions can be defined. In this paper, we will prove that the standard set-theoretic model of the ordinary typed lambda calculus cannot be extended to model this language extension.