*Result*: This Type for Object-Oriented Languages: From Theory to Practice.

*In object-oriented programs, objects often provide methods whose parameter types or return types are he object types themselves. For example, the parameter types of binary methods are the types of their eceiver objects, and the return types of some factory methods are the types of their enclosing objects. owever, most object-oriented languages do not support such methods precisely because their type systems o not support explicit recursive types, which lead to a mismatch between subclassing and subtyping. This ismatch means that an expression of a subclass may not always be usable in a context where an expression f a superclass is expected, which is not intuitive in an object-oriented setting. Researchers have proposed arious type-sound approaches to support methods with types of their enclosing object types denoted by ome variants of ThisType, but they reject reasonable and useful methods due to unpermissive type systems r they use less precise declared inexact types rather than runtime exact types. n this article, we present a thorough approach to support methods with ThisTypes: from a new encoding f objects in a typed lambda calculus that allows subtyping by subclassing to an open-source implementation s an extension of the Java programming language. We first provide real-world examples that motivate he need for ThisTyped methods to precisely describe desired properties of programs. We define a new bject encoding that enables subtyping by subclassing even in the presence of negative occurrences of type ecursion variables by distinguishing object types from existential object types. Based on this object encoding, e formalize language features to support ThisTyped methods with a core calculus CoreThisJava, and prove ts type soundness. Finally, we provide ThisJava, a prototype implementation of the calculus, to show its ackward compatibility, and we make it publicly available. We believe that our approach theoretically xpands the long pursuit of an object-oriented language with ThisTypes to support more useful methods with more precise types. [ABSTRACT FROM AUTHOR]*