类型系统的λω×_≤等式理论及其语义的合理性

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

类型系统在研究程序设计语言的理论基础方面起着十分重要的作用,特别地,带子类型的多态类型系统可刻画面向对象程序设计语言核心概念,如子类型、多态性等.为研究面向对象程序设计语言的形式理论基础,探讨了一个命名为类型系统λω×≤的带高阶子类型的多态类型系统,并利用插入子和fibration理论,引入λω×≤fibration作为该类型系统的语义模型.进一步,讨论了类型系统λω×≤的等式理论,特别是与受限全称量词有关的等式,并利用插入子的性质,证明了对于该等式理论,λω×≤fibration是合理的语义模型.

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 objectoriented 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.