For type theory of object oriented programming, see .
There are many models for object oriented programming language concepts. Often type theory of OO is expressed in terms of category theory for modelling functions and abstractions, and domain theory for modelling recursive definitions. Usual models in terms of category theory use final coalgebras   to model classes of objects from OO - with recursive types and existentially quantified types used for modelling stateful externally visible behaviour and references to (state of) objects. Methods are typed by signatures. Usually subtyping is preferred to subclassing to focus on interfaces rather than implementations. In such models, subclass coercions that model both downcasts and upcadts between object classes are just functions that preserve the external behaviour, subject to constraints requiring preservation of the hidden contents of existentially quantified "OO object state" (preserve the coalgebra structure and contents of existential packages). Downcasts specifically can be modelled as inverses to an "upcast" projection functions that forget some operations and state - notice the failure possibility from such operation must be carefully modelled, usually in terms of Maybe monad modelling partiality.
Notice though that object oriented programming does not in general have a common theoretical foundation, and many programming language concepts are language specific. Theoretical models usually only address public behaviour of systems consisting of OO objects, and try to abstract out the internal implementation details - i.e. primarily modelling interfaces. The models are sometimes used in discussions on language design and for implementation of compilers for the languages . The theoretical models usually use same foundation that is used for modelling functional programming, to unify the foundational concepts.
A complication that often comes up when discussing theoretical models of object oriented programming is the covariance and contravariance of method signatures with respect to subclassing and subtyping relations. Different parts of the OO object model behave differently with respect to whether subclass and subtype relationships allow generalization or specialization of the corresponding method and function signatures and state, and theoretical models spend lots of time discussing when covariance or contravariance is appropriate. The subclassing relation is very complicated as a consequence, and usual approaches on abstracting that can produce unreadable descriptions involving order relationship between models of class types.
 Abadi, Cardelli: "A Theory of Objects", http://lucacardelli.name/indexPast.html
 Poll: "Coalgebraic semantics of subtyping"
 Crole: "Categories for Types"
 Muchnick: Advanced Compiler Design and Implementation"