Type Inference for Recursively Constrained Types and its Application to OOP

This is the authors' abstract. We don't add key points for this paper.

We define a powerful type inference mechanism with application to object-oriented programming. The types inferred are recursively constrained types, types that come with a system of constraints. These types may be viewed as generalizations of recursive types and F-bounded polymorphic types, the forms of type that are necessary to properly encode object typings. The base language we study, I-Soop, incorporates state and records, the two features critical to encode objects in a non-object-oriented language. Soundness and completeness of the type inference algorithm are established by operational means. Our method for establishing these properties is somewhat novel. We illustrate how the algorithm may be fruitfully applied to infer types of object-oriented programs.