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

摘要：

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

关键词：类型系统λω×≤、高阶子类型、等式理论、λω×≤fibration

所属期刊栏目：43

分类号：TP311(计算技术、计算机技术)

资助基金：中国科学院资助项目60403013;广东省博士启动基金031542

在线出版日期：2006-06-01（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：874-880