CPO-MODELS FOR 2ND-ORDER LAMBDA-CALCULUS WITH RECURSIVE TYPES AND SUBTYPING

In this paper we present constructions of cpo models for second order lambda calculi with recursive types and/or subtyping, that are compatible with conventional denotational semantics. For each of the systems we consider, the general structure of an environment model for that system is described first. For the systems with subtyping we prove coherence, i. e. that the meaning of a term is independent of which particular type derivation we consider. The actual model constructions are then based on a standard fixed-point result for omega-categories. The combination and interaction of recursive types and subtyping does not pose any problems.