Polymorphic lambda calculus and subtyping

AbstractWe present a denotational model for F⊑, the extension of second-order lambda calculus with subtyping defined in Cardelli and Wegner (ACM Comput. Surveys 17(4) (1985) 471–522.) Types are interpreted as arbitrary cpos and elements of types as natural transformations. We prove the soundness of our model with respect to the equational theory of F⊑ (Cardelli et al. (Internat. Conf. on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, vol. 526, Springer, Berlin, 1991, pp. 750–770)) and show coherence. Our model is of independent interest, because it integrates ad hoc and parametric polymorphism in an elegant fashion, admits nontrivial records and record update operations, and formalizes an “order faithfulness” criterion for well-behaved multiple subtyping