高级检索
    周晓聪. 类型系统的λω×\-≤等式理论及其语义的合理性[J]. 计算机研究与发展, 2006, 43(5): 874-880.
    引用本文: 周晓聪. 类型系统的λω×\-≤等式理论及其语义的合理性[J]. 计算机研究与发展, 2006, 43(5): 874-880.
    Zhou Xiaocong. Equation Theory of Type System λω×\-≤ and the Soundness of Its Semantics[J]. Journal of Computer Research and Development, 2006, 43(5): 874-880.
    Citation: Zhou Xiaocong. Equation Theory of Type System λω×\-≤ and the Soundness of Its Semantics[J]. Journal of Computer Research and Development, 2006, 43(5): 874-880.

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

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

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

       

      Abstract: 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.

       

    /

    返回文章
    返回