| 类型系统的λω×≤等式理论及其语义的合理性 |
| |
| 引用本文： | 周晓聪.类型系统的λω×≤等式理论及其语义的合理性[J].计算机研究与发展,2006,43(5):874-880. |
| |
| 作者姓名： | 周晓聪 |
| |
| 作者单位： | 中山大学计算机科学系,广州,510275 |
| |
| 基金项目： | 中国科学院资助项目;广东省博士启动基金 |
| |
| 摘 要： | 类型系统在研究程序设计语言的理论基础方面起着十分重要的作用,特别地,带子类型的多态类型系统可刻画面向对象程序设计语言核心概念,如子类型、多态性等.为研究面向对象程序设计语言的形式理论基础,探讨了一个命名为类型系统λω×≤的带高阶子类型的多态类型系统,并利用插入子和fibration理论,引入λω×≤fibration作为该类型系统的语义模型.进一步,讨论了类型系统λω×≤的等式理论,特别是与受限全称量词有关的等式,并利用插入子的性质,证明了对于该等式理论,λω×≤fibration是合理的语义模型.
|
| 关 键 词： | 类型系统λω×≤ 高阶子类型 等式理论 λω×≤fibration |
| 修稿时间： | 2005年3月8日 |
Equation Theory of Type System λω×≤and the Soundness of Its Semantics |
| |
| 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. |
| |
| Authors: | Zhou Xiaocong |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
