作者搜索 |
 |
新闻 |
 10.5.5C-DBLP系统正式发布作者研究兴趣及学术活动展示功能，请访问作者页面试用。
|
|
09.7.6 C-DBLP的文献BibTex信息展示功能正式上线，请访问文章详细页面使用。
|
|
09.7.29 C-DBLP系统新增同名区分功能，欢迎大家在作者页面试用。该功能部分使用了清华大学王建勇老师课题组提出的GHOST（GrapH-based framewOrk for name diStincTion）算法，在此表示感谢。
|
|
09.6.2 C-DBLP系统集成了作者的相关图片并在搜索结果页面展示，敬请试用。
|
| 类型系统λω×≤的范畴论模型 BibTex | |
| 作者： | 周晓聪 李文军 李师贤 |
| 单位： | 中山大学计算机科学系 广州510275 (周晓聪;李文军);中山大学计算机科学系 广州510275(李师贤) |
| 关键词： | 高阶子类型关系;带序范畴;插入子;转换结构 |
| 出处： | 计算机研究与发展 2002 年 01期 |
| 基金： | 高等学校博士学科点专项科研基金资助 (980 5 5 80 1) |
| 全文链接： | 查看全文>> |
| 摘要： | |
| 类型系统一直是理论计算机科学的研究热点 ,特别是带高阶子类型的多态类型系统的研究在探讨面向对象技术形式化理论基础中起着重要作用 .不过至今为止人们还没有得到高阶子类型满意的语义模型 .λω× ≤fibration的基范畴是特殊的带序范畴 ,且有插入子 ,其 fibre范畴是带转换结构的笛卡儿封闭范畴 .λω× ≤ fibration可作为带高阶子类型的多态类型系统的通用范畴论语义模型 | |
| 正文快照： | |
| 1 引 言类型系统一直是理论计算机科学的研究热点 ,特别是提出多态性和子类型的概念以来 ,考察带子类型的多态类型系统已成为面向对象技术的形式理论基础研究的重要内容[1,2 ] .虽然子类型是研究面向对象类型系统的核心概念 ,但高阶子类型关系的语义解释一直是个难题 [3 ] .在此研究领域 ,走出关键一步的是 Phoa提出的包含射 [4]和 Jacobs提出的 subtype fibration[5] ,他们给出的范畴论模型可用于解释类型之间的子类型关系 .我们发现 ,要建立高阶子类型的范畴论模型的关键问题在于两点 :( 1 )给出一般算子之间子类型关系的语义解释 ,… | |
| A CATEGORICAL MODEL OF TYPE SYSTEM λω×≤ | |
| Author： | ZHOU Xiao Cong;LI Wen Jun;and LI Shi Xian (Department of Computer Science;Zhongshan University;Guangzhou 510275) |
| Keywords： | high order subtyping, order enriched category, inserter, coercion structure |
| Abstract： | |
| In recent years, peoples have studied many type systems, and the type systems with high order subtyping play an important role in the research of formal foundation of object oriented technology. But the researchers have not yet got the perfect semantic model for high order subtyping. λω × ≤ fibration can be regarded as the categorical semantic model of high order subtyping. Its base category is the special enriched order category with inserter, and its fibre category is the Cartesian closed category with coercion structure. | |