Polymorphic lambda calculus and subtyping

We present a denotational model for F-subset of or equal to 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 out, model with respect to the equational theory of F-subset of or equal to (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. (C) 2002 Elsevier Science B.V. All rights reserved.