Summary: We define a powerful type inference mechanism with application to object-oriented programming. The types inferred are recursivelyconstrained 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.
For the entire collection see [Zbl 0903.00064].