Matching for the lambda calculus of objects

AbstractA relation between recursive object types, called matching, has been proposed [8] to provide an adequate typing of inheritance in class-based languages.This paper investigates the role of this relation in the design of a type system for the Lambda Calculus of Objects [15]. A new type system for this calculus is defined that uses implicit matchbounded quantification over type variables instead of implicit quantification over row schemes — as in [15] — to capture MyType polymorphic types for methods. An operational semantics is defined for the untyped calculus and type soundness for the new system is proved as a corollary of a subject reduction property. A formal analysis of the relative expressive power of the two systems is also carried out, that explains how the row schemes of [15] can be understood in terms of matching, and shows that the new system is as powerful as the original one on derivations of typing judgements for closed objects