A modest model of records, inheritance, and bounded quantification (Q922718)

The paper presents a formal semantics for the language bounded fun from Cardelli and Wegner (1985). Bounded fun is an extension of second-order lambda calculus supporting both parametric and subtype (inheritance) polymorphism. Partial equivalence relations are used to model inheritance in this language in the presence of subtype and record types. The technical part begins with an introduction to the typed lambda calculus with records and subtypes. It follows a discussion of its model- theoretic semantics based on partial equivalence relations. Syntax and semantics of the language minimal bounded fun and an extension of it are presented, which are modifications of bounded fun. Based on these languages, the semantics of bounded fun itself can be defined. A generalization of partial equivalence relations, called \(\omega\)-sets, are used in combination with modest sets to provide a model of bounded fun with explicit polymorphism. The paper ends with a discussion of principal problems arising with the chosen approach and its relation to other recent work.