Equation Theory of Type System λω×\-≤ and the Soundness of Its Semantics

Type system plays an important role in the research of the foundations of programming language. In particular, the polymorphic type systems with subtyping capture the key concepts of object-oriented programming language such as subtyping and polymorphism. A polymorphic type system with higher-order subtyping, which is called the type system λω×\-≤, is investigated. By using the inserters and the theory of fibrations, a kind of fibration called the λω×\-≤ fibration is introduced as the semantic model of the type system λω×\-≤. In this paper, the equation theory of the type system λω×\-≤, especially, the equations related to the bounded quantification type, are discussed. Furthermore, by using the properties of the inserters, the semantic soundness of the λω×\-≤ fibration with respect to the equation theory of the type system λω×\-≤ is shown.