中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
类型系统及其范畴论模型研究
作者: 周晓聪
答辩日期: 2000
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 高阶子类型 ; 受限量词类型 ; 带序范畴 ; 插入子 λω×<,≤>fibration ; PER模型
摘要: 该文提出带高阶子类型的多态类型系统λω×<,≤>,它是[Cro193]的类型系统λω×的扩充,为一般算子引入了子类型关系,并结合多态性使用了受限量词类型,与已有的各种系统F的扩充相比,其特点是区分了各种上下文,使得整个类型系统在逻辑上更严谨,也可更好地研究其语义模型.该文详细研究了类型系统λω×<,≤>的各种结构性质.该文提出λω×<,≤>fibration作为高阶子类型的语义模型,其核心是引入了带序范畴及其插入子的概念,从而将λω×<,≤>fibration基范畴的射之间的关系与全范畴的对象之间关系结合在一起,给出了一般算子之间子类型关系的语义解释,解决了在[CL91]中所说的子类型关系的通用范畴论模型问题.该文的λω×<,≤>fibration结合了[Jaco95]中定义的subtypingfibration和[Phoa92b]中提出的包含射的优点,完整地给出了受限量词的范畴论语义解释,并很好地解释了一般算子之间子类型关系以及有关子类型关系的结构性质,完整地给出了已证明项的语义模型,也给出了有关已证明项的各种结构性质规则的语义解释,证明了该模型对于已证明项的等式理论的合理性.
英文摘要: Type system is a hot point of the theoretical research in computer science. It takes important application in the design of new programming language and the development of the compiler of new language. In the recent years, with the wide application of object-oriented language, many peoples have studied the type system of object-oriented language deeply. In object-oriented type system, polymorphism and subtype is the core concept. Many peoples have studied the semantic model of polymorphism and subtype. Especially those model based on category theory have been studied widely. Category theory, which is a branch of universal algebraic, have been used widely in theoretical computer science, such as formal semantics, computational model and high-order logic. The key concept of category theory, for example, discover the properties of object through studying its out-look behaviors, have the natural relation with the core concept of object-oriented technology. We believe that category theory will take the important role in the research of the foundations of object-oriented technology. In this thesis, we give a type system named Xcoxs, which is the extension of type systemλω×<,≤in [Crol93]. We introduced subtype relation for all operators and used bounded quantification type. Comparing with those extension of system F, our system distinguished three kind context, that is operator context, subtyping context and term context. Our system has the strict logic, and is easy to study its categorical model. In this thesis, we have study its structural properties in detail in chapter 5. We provideλω×<,≤fibration as the semantic model of high-order subtyping. The key point ofλω×<,≤fibration are inserter, which give a good bridge between the subtype relation of morphism in base category and the subtype relation of object in total category. The Xcoxs fibration, which combine the ideal of subtyping fibration in [Jaco95] and inclusion map in [Phoa92b], interpret the semantic of bounded quantification completely, and can give the semantic model of subtype relation of all operator. We discuss the semantic interpretation of the structural properties of subtyping and typing rules of type sytem Xcoxs, and proved the soundness theorem of our semantic model. We think we have made a broke progress of the semantic model of high-order subtyping.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6772
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW008615.pdf(2712KB)----限制开放-- 联系获取全文

Recommended Citation:
周晓聪. 类型系统及其范畴论模型研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[周晓聪]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[周晓聪]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace