Abstract: Type system is an important tool for studying the formal foundations of object oriented technique Type system λω × ≤ is a polymorphism type system with higher order subtyping, and its properties and categorical semantic model are studied How to explore the formal semantics of the key concepts of object oriented technique, such as object, class, inheritance etc , is explained by using type system λω × ≤ Taking class POINT and CPOINT as examples, two object encoding methods, the recursive type based method and the existential type based method are discussed, and how to encode that two classes in type system λω × ≤ is investigated Further, the features of that two object encoding methods are summarized and compared