期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
308
篇文章
<
1
2
…
16
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
安全类型系统在编译技术中的应用研究
1
作者
赵秀凤
杨丽娜
郭渊博
《计算机工程与科学》
CSCD
2008年第9期145-146,157,共3页
类型系统是一种设计和研究程序设计语言的形式化方法和工具。本文提出了一种新的用安全类型系统增强编译程序安全性的方法;给出了类型系统的形式化定义,引入了安全类型和安全类型系统的概念,并给出了安全类型系统的子类型规则和安全类...
类型系统是一种设计和研究程序设计语言的形式化方法和工具。本文提出了一种新的用安全类型系统增强编译程序安全性的方法;给出了类型系统的形式化定义,引入了安全类型和安全类型系统的概念,并给出了安全类型系统的子类型规则和安全类型规则;最后讨论了安全类型系统在编译技术中的应用。
展开更多
关键词
类型系统
安全
类型系统
编译
子
类型
规则
安全
类型
规则
下载PDF
职称材料
类型系统的构造、实现及其在程序设计语言中的应用
被引量:
3
2
作者
蒋慧
张兴元
+1 位作者
王元元
谢希仁
《南京大学学报(自然科学版)》
CAS
CSCD
北大核心
2001年第2期199-207,共9页
类型系统是一种设计和研究程序设计语言的形式化方法和工具 ,既可在语言设计之初构造 ,便于严格、准确、正确地设计实现语言 ;也可在语言实现后构造 ,为研究语言的语义及其它性质建立模型 .详细讨论了类型系统的基本构造和实现 ,通过基...
类型系统是一种设计和研究程序设计语言的形式化方法和工具 ,既可在语言设计之初构造 ,便于严格、准确、正确地设计实现语言 ;也可在语言实现后构造 ,为研究语言的语义及其它性质建立模型 .详细讨论了类型系统的基本构造和实现 ,通过基于图重写的函数式语言SClean的类型系统 。
展开更多
关键词
类型系统
类型
推理
类型
检测
语义模型
程序设计语言
构造
形式化工具
形式化方法
下载PDF
职称材料
类型系统λω×≤的范畴论模型
被引量:
4
3
作者
周晓聪
李文军
李师贤
《计算机研究与发展》
EI
CSCD
北大核心
2002年第1期68-72,共5页
类型系统一直是理论计算机科学的研究热点 ,特别是带高阶子类型的多态类型系统的研究在探讨面向对象技术形式化理论基础中起着重要作用 .不过至今为止人们还没有得到高阶子类型满意的语义模型 .λω× ≤fibration的基范畴是特殊的...
类型系统一直是理论计算机科学的研究热点 ,特别是带高阶子类型的多态类型系统的研究在探讨面向对象技术形式化理论基础中起着重要作用 .不过至今为止人们还没有得到高阶子类型满意的语义模型 .λω× ≤fibration的基范畴是特殊的带序范畴 ,且有插入子 ,其 fibre范畴是带转换结构的笛卡儿封闭范畴 .λω× ≤
展开更多
关键词
高阶子
类型
关系
带序范畴
计算机科学
类型系统
范畴论模型
下载PDF
职称材料
类型系统λω×≤
被引量:
3
4
作者
周晓聪
李文军
李师贤
《中山大学学报(自然科学版)》
CAS
CSCD
北大核心
2001年第3期13-17,共5页
为研究高阶子类型的范畴论语义模型 ,区分了带高阶子类型的类型系统中的各种上下文 ,并简化其中的受限全称量词类型引入规则 ,而提出了类型系统λω×≤ .文章介绍该类型系统有关类别 (Kind)、算子 (Operator)、项 (Term)的规则 ,...
为研究高阶子类型的范畴论语义模型 ,区分了带高阶子类型的类型系统中的各种上下文 ,并简化其中的受限全称量词类型引入规则 ,而提出了类型系统λω×≤ .文章介绍该类型系统有关类别 (Kind)、算子 (Operator)、项 (Term)的规则 ,及其与建立范畴论语义模型有关的结构性质 .
展开更多
关键词
类型系统
子
类型
受限全称量词
类型
语义模型
面向对象技术
下载PDF
职称材料
类型系统λω×≤的PER模型
被引量:
3
5
作者
周晓聪
李文军
李师贤
《计算机研究与发展》
EI
CSCD
北大核心
2000年第8期1006-1011,共6页
类型系统是近年来理论计算机科学的研究热点之一 .1999年周晓聪曾在文献 [1]中提出并研究了类型系统λω× ≤ 及其性质 .类型系统λω× ≤ 是λω×的扩充 ,引入了子类型关系和受限的全称类型 .与 System F的各种扩充相...
类型系统是近年来理论计算机科学的研究热点之一 .1999年周晓聪曾在文献 [1]中提出并研究了类型系统λω× ≤ 及其性质 .类型系统λω× ≤ 是λω×的扩充 ,引入了子类型关系和受限的全称类型 .与 System F的各种扩充相比 ,它区分各种上下文 ,使得规则和性质的研究更为清晰 .研究该类型系统的 PER模型作为其语义解释 。
展开更多
关键词
类型系统
子
类型
关系
PER模型
面向对象
下载PDF
职称材料
Gdel语言类型系统
被引量:
3
6
作者
王炳波
赵致琢
晏松
《计算机工程与设计》
CSCD
北大核心
2005年第12期3432-3435,3438,共5页
Gdel语言是一种说明性逻辑程序设计语言。该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义。详细介绍了Gdel语言的类型系统及其构造,...
Gdel语言是一种说明性逻辑程序设计语言。该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义。详细介绍了Gdel语言的类型系统及其构造,对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论。
展开更多
关键词
Goedel
PROLOG
类型系统
多态多类
类型
推理
下载PDF
职称材料
类型系统与程序正确性问题
被引量:
3
7
作者
丁志义
宋国新
邵志清
《计算机科学》
CSCD
北大核心
2006年第1期141-143,157,共4页
类型系统能检出合法程序的语义错误,可以缩短调试时间,在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统...
类型系统能检出合法程序的语义错误,可以缩短调试时间,在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统,因而类型系统可以表迭程序的性质,并自动进行验证。
展开更多
关键词
类型系统
程序验证
Λ演算
证明理论
程序正确性
语义错误
执行程序
直觉主义
子
类型
代码
下载PDF
职称材料
类型系统的研究与进展
被引量:
2
8
作者
周晓聪
李文军
李师贤
《计算机科学》
CSCD
北大核心
2000年第5期5-13,共9页
1 引言类型系统源于罗素为避免朴素集合论中的悖论而引入的“分类”思想。后来邱奇在他的λ演算中也引入了“类型”。60年代初出现的Algol语言提出了数据类型的概念。逻辑学家J.Girard和计算机科学家J.Reynold在70年代初为类型系统引入...
1 引言类型系统源于罗素为避免朴素集合论中的悖论而引入的“分类”思想。后来邱奇在他的λ演算中也引入了“类型”。60年代初出现的Algol语言提出了数据类型的概念。逻辑学家J.Girard和计算机科学家J.Reynold在70年代初为类型系统引入了“多态性”,分别提出了System F和多态λ演算。另一方面,Mar-tin-L of为了研究数学的逻辑基础,在70年代初提出了直觉类型理论,后来也用于程序开发的研究。 80年代后,类型系统的研究更是蓬勃发展,在程序语言设计、程序开发和验证以及机器定理证明方面得到了广泛的应用。目前随着面向对象思想逐渐占据软件开发的主流,面向对象程序设计语言的类型系统逐渐成为人们研究的热点。在80年代初,L.Cardelli提出了“子类型”(subtype)的概念,在1985年。
展开更多
关键词
类型系统
Λ演算
面向对象
软件开发
下载PDF
职称材料
基于类型系统的元数据模型
被引量:
4
9
作者
陈睿
蔡希尧
《软件学报》
EI
CSCD
北大核心
1995年第5期265-275,共11页
本文研究了程序设计语言的类型系统与数据模型的关系,认识到类型间关系是表示数据模型的一种方法.基于这一思想,提出了PCT类型描述语言及基于PCT的元数据模型,以描述多种数据模型.PCT将C++类型系统与一阶谓词演算相结...
本文研究了程序设计语言的类型系统与数据模型的关系,认识到类型间关系是表示数据模型的一种方法.基于这一思想,提出了PCT类型描述语言及基于PCT的元数据模型,以描述多种数据模型.PCT将C++类型系统与一阶谓词演算相结合,可以形式化地描述特定数据模型所规定的多方面规范.
展开更多
关键词
数据模型
数据
类型
程序语言
类型系统
下载PDF
职称材料
一种带约束的多态类型系统
被引量:
3
10
作者
郑红军
张乃孝
《计算机学报》
EI
CSCD
北大核心
1999年第4期343-350,共8页
本文讨论了一种带约束的多态类型系统,引入了约束类型.约束与全称量化的结合使得参数化多态函数的应用更安全,同时也为重载的表示和实现提供了一个新的途径,提高了类型表示的抽象度本文讨论的类型系统具有两个不同层次的类型结构,...
本文讨论了一种带约束的多态类型系统,引入了约束类型.约束与全称量化的结合使得参数化多态函数的应用更安全,同时也为重载的表示和实现提供了一个新的途径,提高了类型表示的抽象度本文讨论的类型系统具有两个不同层次的类型结构,约束的引入与消去是不同层次上的操作.最后,本文绘出了类型检查算法Wτ,并证明了此算法中约束的可满足性是可判定的.
展开更多
关键词
约束
类型
类型
检查
多态
类型系统
程序设计语言
下载PDF
职称材料
对象在类型系统λω×≤中的表示
被引量:
1
11
作者
周晓聪
李文军
李师贤
《计算机研究与发展》
EI
CSCD
北大核心
2003年第4期517-523,共7页
类型系统是研究面向对象技术形式理论基础的重要工具 类型系统λω×≤ 是一个带高阶子类型关系的多态类型系统 ,对其性质和范畴论语义模型进行了研究 在此基础上 ,讨论了如何以类型系统λω× ≤ 为工具 ,研究对象、类、继...
类型系统是研究面向对象技术形式理论基础的重要工具 类型系统λω×≤ 是一个带高阶子类型关系的多态类型系统 ,对其性质和范畴论语义模型进行了研究 在此基础上 ,讨论了如何以类型系统λω× ≤ 为工具 ,研究对象、类、继承等面向对象技术的基本概念的形式语义 结合类POINT和CPOINT等例子 ,讨论了基于递归类型和基于存在类型的两种对象表示方法 。
展开更多
关键词
对象表示
面向对象
类型系统
λω×≤
程序设计
递归
类型
存在
类型
下载PDF
职称材料
建立保护区经营类型系统促进我国保护区事业的发展
被引量:
4
12
作者
刘东来
《林业科学》
EI
CAS
CSCD
北大核心
1996年第6期553-563,共11页
国际保护组织IUCN提出把保护区区分为类型有1/4世纪了,对保护和合理利用资源取得了相当的成就和经验。我国在这方面尚属空白。本文一方面介绍国际上保护区区分类型的背景、目的以及1978年和1994年IUCN、CNPPA推荐的两个经营类型系统...
国际保护组织IUCN提出把保护区区分为类型有1/4世纪了,对保护和合理利用资源取得了相当的成就和经验。我国在这方面尚属空白。本文一方面介绍国际上保护区区分类型的背景、目的以及1978年和1994年IUCN、CNPPA推荐的两个经营类型系统,引荐国际保护区经营类型系统和应用经营类型的实例;另方面在此基础上提出我国的保护区经营类型系统。希望能有助于我国保护区事业特别是经营工作的发展。
展开更多
关键词
保护区
经营
类型系统
经营
类型
经营目的
下载PDF
职称材料
类型系统的λω×_≤等式理论及其语义的合理性
被引量:
2
13
作者
周晓聪
《计算机研究与发展》
EI
CSCD
北大核心
2006年第5期874-880,共7页
类型系统在研究程序设计语言的理论基础方面起着十分重要的作用,特别地,带子类型的多态类型系统可刻画面向对象程序设计语言核心概念,如子类型、多态性等.为研究面向对象程序设计语言的形式理论基础,探讨了一个命名为类型系统λω×...
类型系统在研究程序设计语言的理论基础方面起着十分重要的作用,特别地,带子类型的多态类型系统可刻画面向对象程序设计语言核心概念,如子类型、多态性等.为研究面向对象程序设计语言的形式理论基础,探讨了一个命名为类型系统λω×≤的带高阶子类型的多态类型系统,并利用插入子和fibration理论,引入λω×≤fibration作为该类型系统的语义模型.进一步,讨论了类型系统λω×≤的等式理论,特别是与受限全称量词有关的等式,并利用插入子的性质,证明了对于该等式理论,λω×≤fibration是合理的语义模型.
展开更多
关键词
类型系统
λω×≤
高阶子
类型
等式理论
λω×≤fibration
下载PDF
职称材料
为π演算建立具有安全级别的简单类型系统(英文)
被引量:
1
14
作者
王立斌
陈克非
《中国科学院研究生院学报》
CAS
CSCD
2002年第3期278-281,共4页
为π演算建立具有安全级别的简单类型系统,并证明该类型系统在规约语义下的类型可靠性.此类型系统使得π演算成为安全系统、安全协议分析与规范的普适形式化工具.
关键词
简单
类型系统
Π演算
安全协议
规约语义
类型
可靠性
安全
系统
计算机安全
下载PDF
职称材料
基于类型系统的完整性信息流控制
被引量:
1
15
作者
王立斌
《华南师范大学学报(自然科学版)》
CAS
2006年第3期42-47,共6页
构造了一种实现完整性信息流控制的安全类型系统.首先,为π-演算建立具有完整性安全等级的安全类型.然后,建立该安全类型的子类规则和类型规则,这些规则实现了系统的完整性策略及对系统行为的限制.最后,证明该类型系统的类型合理性,表...
构造了一种实现完整性信息流控制的安全类型系统.首先,为π-演算建立具有完整性安全等级的安全类型.然后,建立该安全类型的子类规则和类型规则,这些规则实现了系统的完整性策略及对系统行为的限制.最后,证明该类型系统的类型合理性,表明满足初始安全策略的系统经过不断的演进、交互,系统的安全属性依然可被满足.所建立的完整性信息流控制机制可通过静态类型检验高效实现.
展开更多
关键词
完整性
类型系统
安全模型
下载PDF
职称材料
面向对象程序设计语言的类型系统
被引量:
1
16
作者
李晓燕
李斌
《小型微型计算机系统》
EI
CSCD
北大核心
2000年第6期650-652,共3页
本文引入了面向对象程序设计语言的类的概念 ,对类及其继承性给出了一种严格的形式化描述 .这种形式化描述显然是建立面向对象模型的基础 .
关键词
面向对象
程序设计语言
类型系统
类
继承性
下载PDF
职称材料
命令的操作语义在类型系统中的一种表示
17
作者
丁志义
宋国新
邵志清
《小型微型计算机系统》
CSCD
北大核心
2006年第7期1285-1288,共4页
类型系统建立在一个小的规则集合基础上,易于实现,可理解性好,且具有计算完全性和足够的表达能力.在类型系统中可以重述推导规则,将其形式化为一些归纳关系,从而直接表示了命令的操作语义.类型理论不仅适合于函数式程序的证明,也是刻画...
类型系统建立在一个小的规则集合基础上,易于实现,可理解性好,且具有计算完全性和足够的表达能力.在类型系统中可以重述推导规则,将其形式化为一些归纳关系,从而直接表示了命令的操作语义.类型理论不仅适合于函数式程序的证明,也是刻画和证明命令式程序的合适的框架.
展开更多
关键词
操作语义
类型
理论
类型系统
程序验证
下载PDF
职称材料
一种基于扩展Spi演算的类型系统
18
作者
袁霖
王亚弟
韩继红
《计算机工程与应用》
CSCD
北大核心
2007年第3期131-134,138,共5页
主要探讨了使用非形式化的原理和形式化的规则来获得密码协议安全属性的方法。这些原理和规则基于传统的等级和信息流的思想,通过将其扩展后用来处理密码协议中的并发进程。提出的规则是基于Spi演算扩展语法的一种类型规则。通过这些规...
主要探讨了使用非形式化的原理和形式化的规则来获得密码协议安全属性的方法。这些原理和规则基于传统的等级和信息流的思想,通过将其扩展后用来处理密码协议中的并发进程。提出的规则是基于Spi演算扩展语法的一种类型规则。通过这些规则可以向用户担保,如果协议通过了类型检测,则该协议没有泄漏任何秘密的消息。
展开更多
关键词
类型系统
密码协议
保密性
类型
规则
下载PDF
职称材料
基于类型理论的XML类型系统形式化建模
19
作者
冯玉才
刘丹
班鹏新
《计算机工程》
EI
CAS
CSCD
北大核心
2004年第12期45-47,共3页
利用形式化模型的形式简洁、描述清晰、逻辑性强、易于扩展以及实用性强等优点,运用基于类型理论的逻辑化形式建模技术对XML类型系统进行了形式化建模,实现了对各种XML数据的类型定义和对XML数据处理过程的类型检验,为可直接存储和检索...
利用形式化模型的形式简洁、描述清晰、逻辑性强、易于扩展以及实用性强等优点,运用基于类型理论的逻辑化形式建模技术对XML类型系统进行了形式化建模,实现了对各种XML数据的类型定义和对XML数据处理过程的类型检验,为可直接存储和检索XML数据的XML数据库DM4提供了一种有效的类型系统设计方案。
展开更多
关键词
XML数据库
XML
类型系统
类型
理论
逻辑化形式建模
下载PDF
职称材料
TTCN-3类型系统测试用例集自动生成
20
作者
蒋凡
金鑫
吴文娟
《计算机系统应用》
2009年第9期45-49,共5页
针对编译器测试中最为重要的测试用例集构造问题,提出了针对TTCN-3语言类型系统的编译器测试用例集层次化、结构化的自动生成方案。语法方面,严格遵从语言规格说明中的扩展巴科斯-瑙尔范式(EBNF);语义正确性上,采用定义"元素定义...
针对编译器测试中最为重要的测试用例集构造问题,提出了针对TTCN-3语言类型系统的编译器测试用例集层次化、结构化的自动生成方案。语法方面,严格遵从语言规格说明中的扩展巴科斯-瑙尔范式(EBNF);语义正确性上,采用定义"元素定义偏序文件"、建立抽象语法树等多种方法加以保证。实验表明新方案极大提高了测试用例集的生成效率,对TTCN-3类型系统语法、语义两方面都达到很好的测试覆盖,增强了发现编译器缺陷的能力。该方案对于其他语言的编译器测试也具有参考价值。
展开更多
关键词
TTCN-3
类型系统
编译器测试
测试用例集自动生成
层次化
结构化方法
下载PDF
职称材料
题名
安全类型系统在编译技术中的应用研究
1
作者
赵秀凤
杨丽娜
郭渊博
机构
解放军信息工程大学电子技术学院
出处
《计算机工程与科学》
CSCD
2008年第9期145-146,157,共3页
基金
国家自然科学基金资助项目(60503012)
文摘
类型系统是一种设计和研究程序设计语言的形式化方法和工具。本文提出了一种新的用安全类型系统增强编译程序安全性的方法;给出了类型系统的形式化定义,引入了安全类型和安全类型系统的概念,并给出了安全类型系统的子类型规则和安全类型规则;最后讨论了安全类型系统在编译技术中的应用。
关键词
类型系统
安全
类型系统
编译
子
类型
规则
安全
类型
规则
Keywords
type system
safe-type system
compilation
sub-type rules
safe-type rule
分类号
TP309 [自动化与计算机技术—计算机系统结构]
TP314 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
类型系统的构造、实现及其在程序设计语言中的应用
被引量:
3
2
作者
蒋慧
张兴元
王元元
谢希仁
机构
解放军理工大学指挥自动化学院计算机系
出处
《南京大学学报(自然科学版)》
CAS
CSCD
北大核心
2001年第2期199-207,共9页
基金
国家自然科学基金! ( 6993 1 0 4 0 )
文摘
类型系统是一种设计和研究程序设计语言的形式化方法和工具 ,既可在语言设计之初构造 ,便于严格、准确、正确地设计实现语言 ;也可在语言实现后构造 ,为研究语言的语义及其它性质建立模型 .详细讨论了类型系统的基本构造和实现 ,通过基于图重写的函数式语言SClean的类型系统 。
关键词
类型系统
类型
推理
类型
检测
语义模型
程序设计语言
构造
形式化工具
形式化方法
Keywords
type system, type inference, type checking, semantic model
分类号
TP312 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
类型系统λω×≤的范畴论模型
被引量:
4
3
作者
周晓聪
李文军
李师贤
机构
中山大学计算机科学系
出处
《计算机研究与发展》
EI
CSCD
北大核心
2002年第1期68-72,共5页
基金
高等学校博士学科点专项科研基金资助 (980 5 5 80 1)
文摘
类型系统一直是理论计算机科学的研究热点 ,特别是带高阶子类型的多态类型系统的研究在探讨面向对象技术形式化理论基础中起着重要作用 .不过至今为止人们还没有得到高阶子类型满意的语义模型 .λω× ≤fibration的基范畴是特殊的带序范畴 ,且有插入子 ,其 fibre范畴是带转换结构的笛卡儿封闭范畴 .λω× ≤
关键词
高阶子
类型
关系
带序范畴
计算机科学
类型系统
范畴论模型
Keywords
high order subtyping, order enriched category, inserter, coercion structure
分类号
TP301 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
类型系统λω×≤
被引量:
3
4
作者
周晓聪
李文军
李师贤
机构
中山大学计算机科学系
出处
《中山大学学报(自然科学版)》
CAS
CSCD
北大核心
2001年第3期13-17,共5页
基金
高等学校博士学科点专项科研基金!资助项目 (980 5 5 80 1)
文摘
为研究高阶子类型的范畴论语义模型 ,区分了带高阶子类型的类型系统中的各种上下文 ,并简化其中的受限全称量词类型引入规则 ,而提出了类型系统λω×≤ .文章介绍该类型系统有关类别 (Kind)、算子 (Operator)、项 (Term)的规则 ,及其与建立范畴论语义模型有关的结构性质 .
关键词
类型系统
子
类型
受限全称量词
类型
语义模型
面向对象技术
Keywords
type system
subtyping
bounded quantification type
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
类型系统λω×≤的PER模型
被引量:
3
5
作者
周晓聪
李文军
李师贤
机构
中山大学计算机科学系
南京大学计算机软件新技术国家重点实验室
出处
《计算机研究与发展》
EI
CSCD
北大核心
2000年第8期1006-1011,共6页
基金
高等学校博士学科点专项科研基金
南京大学计算机软件新技术国家重点实验室基金
文摘
类型系统是近年来理论计算机科学的研究热点之一 .1999年周晓聪曾在文献 [1]中提出并研究了类型系统λω× ≤ 及其性质 .类型系统λω× ≤ 是λω×的扩充 ,引入了子类型关系和受限的全称类型 .与 System F的各种扩充相比 ,它区分各种上下文 ,使得规则和性质的研究更为清晰 .研究该类型系统的 PER模型作为其语义解释 。
关键词
类型系统
子
类型
关系
PER模型
面向对象
Keywords
type system, subtype relation, PER model
分类号
TP311.11 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
Gdel语言类型系统
被引量:
3
6
作者
王炳波
赵致琢
晏松
机构
厦门大学计算机科学系
出处
《计算机工程与设计》
CSCD
北大核心
2005年第12期3432-3435,3438,共5页
文摘
Gdel语言是一种说明性逻辑程序设计语言。该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义。详细介绍了Gdel语言的类型系统及其构造,对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论。
关键词
Goedel
PROLOG
类型系统
多态多类
类型
推理
Keywords
goedel
prolog
type system
polymorphicmany-sorted
type deduction
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
类型系统与程序正确性问题
被引量:
3
7
作者
丁志义
宋国新
邵志清
机构
华东理工大学计算机科学与工程系
出处
《计算机科学》
CSCD
北大核心
2006年第1期141-143,157,共4页
基金
本文工作得到国家自然科学基金和中科院计算机科学重点实验室资助(编号:60373075
SYSKF0305)。
文摘
类型系统能检出合法程序的语义错误,可以缩短调试时间,在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统,因而类型系统可以表迭程序的性质,并自动进行验证。
关键词
类型系统
程序验证
Λ演算
证明理论
程序正确性
语义错误
执行程序
直觉主义
子
类型
代码
Keywords
Type system, Program verification, λ-calculus, Proof theory
分类号
TP311.1 [自动化与计算机技术—计算机软件与理论]
TP312 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
类型系统的研究与进展
被引量:
2
8
作者
周晓聪
李文军
李师贤
机构
中山大学计算机科学系
出处
《计算机科学》
CSCD
北大核心
2000年第5期5-13,共9页
基金
高等学校博士学科点专项科研基金
资助号:99-018-411703
文摘
1 引言类型系统源于罗素为避免朴素集合论中的悖论而引入的“分类”思想。后来邱奇在他的λ演算中也引入了“类型”。60年代初出现的Algol语言提出了数据类型的概念。逻辑学家J.Girard和计算机科学家J.Reynold在70年代初为类型系统引入了“多态性”,分别提出了System F和多态λ演算。另一方面,Mar-tin-L of为了研究数学的逻辑基础,在70年代初提出了直觉类型理论,后来也用于程序开发的研究。 80年代后,类型系统的研究更是蓬勃发展,在程序语言设计、程序开发和验证以及机器定理证明方面得到了广泛的应用。目前随着面向对象思想逐渐占据软件开发的主流,面向对象程序设计语言的类型系统逐渐成为人们研究的热点。在80年代初,L.Cardelli提出了“子类型”(subtype)的概念,在1985年。
关键词
类型系统
Λ演算
面向对象
软件开发
Keywords
X calculus,Type system,Programming type system,Logical type system
分类号
TP311.52 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于类型系统的元数据模型
被引量:
4
9
作者
陈睿
蔡希尧
机构
华南理工大学计算机系
出处
《软件学报》
EI
CSCD
北大核心
1995年第5期265-275,共11页
基金
国家教委博士点基金
文摘
本文研究了程序设计语言的类型系统与数据模型的关系,认识到类型间关系是表示数据模型的一种方法.基于这一思想,提出了PCT类型描述语言及基于PCT的元数据模型,以描述多种数据模型.PCT将C++类型系统与一阶谓词演算相结合,可以形式化地描述特定数据模型所规定的多方面规范.
关键词
数据模型
数据
类型
程序语言
类型系统
Keywords
Data model,object-oriented programming,data type, first order predicate calculus.
分类号
TP312 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
一种带约束的多态类型系统
被引量:
3
10
作者
郑红军
张乃孝
机构
北京大学数学学院信息科学系
出处
《计算机学报》
EI
CSCD
北大核心
1999年第4期343-350,共8页
文摘
本文讨论了一种带约束的多态类型系统,引入了约束类型.约束与全称量化的结合使得参数化多态函数的应用更安全,同时也为重载的表示和实现提供了一个新的途径,提高了类型表示的抽象度本文讨论的类型系统具有两个不同层次的类型结构,约束的引入与消去是不同层次上的操作.最后,本文绘出了类型检查算法Wτ,并证明了此算法中约束的可满足性是可判定的.
关键词
约束
类型
类型
检查
多态
类型系统
程序设计语言
Keywords
Polymorphism, constrained type, type system. type checking
分类号
TP312 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
对象在类型系统λω×≤中的表示
被引量:
1
11
作者
周晓聪
李文军
李师贤
机构
中山大学计算机科学系
出处
《计算机研究与发展》
EI
CSCD
北大核心
2003年第4期517-523,共7页
基金
高等学校博士学科点专项科研基金
广东省教育厅软件技术重点实验室项目基金
文摘
类型系统是研究面向对象技术形式理论基础的重要工具 类型系统λω×≤ 是一个带高阶子类型关系的多态类型系统 ,对其性质和范畴论语义模型进行了研究 在此基础上 ,讨论了如何以类型系统λω× ≤ 为工具 ,研究对象、类、继承等面向对象技术的基本概念的形式语义 结合类POINT和CPOINT等例子 ,讨论了基于递归类型和基于存在类型的两种对象表示方法 。
关键词
对象表示
面向对象
类型系统
λω×≤
程序设计
递归
类型
存在
类型
Keywords
object encoding
recursive type
existential type
分类号
TP311.1 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
建立保护区经营类型系统促进我国保护区事业的发展
被引量:
4
12
作者
刘东来
机构
中国林业科学研究院
出处
《林业科学》
EI
CAS
CSCD
北大核心
1996年第6期553-563,共11页
文摘
国际保护组织IUCN提出把保护区区分为类型有1/4世纪了,对保护和合理利用资源取得了相当的成就和经验。我国在这方面尚属空白。本文一方面介绍国际上保护区区分类型的背景、目的以及1978年和1994年IUCN、CNPPA推荐的两个经营类型系统,引荐国际保护区经营类型系统和应用经营类型的实例;另方面在此基础上提出我国的保护区经营类型系统。希望能有助于我国保护区事业特别是经营工作的发展。
关键词
保护区
经营
类型系统
经营
类型
经营目的
Keywords
Protected area, Management category system, Management category,Management objectives, Categorisation
分类号
S759.9 [农业科学—森林经理学]
下载PDF
职称材料
题名
类型系统的λω×_≤等式理论及其语义的合理性
被引量:
2
13
作者
周晓聪
机构
中山大学计算机科学系
出处
《计算机研究与发展》
EI
CSCD
北大核心
2006年第5期874-880,共7页
基金
国家自然科学基金项目(60403013)
广东省自然科学基金项目(031542)~~
文摘
类型系统在研究程序设计语言的理论基础方面起着十分重要的作用,特别地,带子类型的多态类型系统可刻画面向对象程序设计语言核心概念,如子类型、多态性等.为研究面向对象程序设计语言的形式理论基础,探讨了一个命名为类型系统λω×≤的带高阶子类型的多态类型系统,并利用插入子和fibration理论,引入λω×≤fibration作为该类型系统的语义模型.进一步,讨论了类型系统λω×≤的等式理论,特别是与受限全称量词有关的等式,并利用插入子的性质,证明了对于该等式理论,λω×≤fibration是合理的语义模型.
关键词
类型系统
λω×≤
高阶子
类型
等式理论
λω×≤fibration
Keywords
type system λω×≤
higher-order subtyping, equation theory
λω×≤ fibration
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
为π演算建立具有安全级别的简单类型系统(英文)
被引量:
1
14
作者
王立斌
陈克非
机构
上海交通大学计算机科学与工程系
出处
《中国科学院研究生院学报》
CAS
CSCD
2002年第3期278-281,共4页
基金
Major Program of National Natural Science Foundation of China (90104005) and General Program of Natural Science Foun-dation of China (69973031)
文摘
为π演算建立具有安全级别的简单类型系统,并证明该类型系统在规约语义下的类型可靠性.此类型系统使得π演算成为安全系统、安全协议分析与规范的普适形式化工具.
关键词
简单
类型系统
Π演算
安全协议
规约语义
类型
可靠性
安全
系统
计算机安全
Keywords
π-calculus, type system, secure protocols
分类号
TP309 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
基于类型系统的完整性信息流控制
被引量:
1
15
作者
王立斌
机构
华南师范大学计算机学院
出处
《华南师范大学学报(自然科学版)》
CAS
2006年第3期42-47,共6页
基金
2004年中国博士后科学基金资助项目
文摘
构造了一种实现完整性信息流控制的安全类型系统.首先,为π-演算建立具有完整性安全等级的安全类型.然后,建立该安全类型的子类规则和类型规则,这些规则实现了系统的完整性策略及对系统行为的限制.最后,证明该类型系统的类型合理性,表明满足初始安全策略的系统经过不断的演进、交互,系统的安全属性依然可被满足.所建立的完整性信息流控制机制可通过静态类型检验高效实现.
关键词
完整性
类型系统
安全模型
Keywords
integrity
type system
security model
分类号
TP309 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
面向对象程序设计语言的类型系统
被引量:
1
16
作者
李晓燕
李斌
机构
华中师范大学计算机科学系
武汉铁路运输学校
出处
《小型微型计算机系统》
EI
CSCD
北大核心
2000年第6期650-652,共3页
文摘
本文引入了面向对象程序设计语言的类的概念 ,对类及其继承性给出了一种严格的形式化描述 .这种形式化描述显然是建立面向对象模型的基础 .
关键词
面向对象
程序设计语言
类型系统
类
继承性
Keywords
Class
Inheritance
Formalization
分类号
TP312 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
命令的操作语义在类型系统中的一种表示
17
作者
丁志义
宋国新
邵志清
机构
华东理工大学计算机科学与工程系
出处
《小型微型计算机系统》
CSCD
北大核心
2006年第7期1285-1288,共4页
基金
国家自然科学基金项目(60373075)资助
教育部科学技术研究重点项目(01077)资助
+1 种基金
中科院计算机科学重点实验室项目(SYSKF0305)资助
上海市科学技术委员会科研计划项目(045115006)资助.
文摘
类型系统建立在一个小的规则集合基础上,易于实现,可理解性好,且具有计算完全性和足够的表达能力.在类型系统中可以重述推导规则,将其形式化为一些归纳关系,从而直接表示了命令的操作语义.类型理论不仅适合于函数式程序的证明,也是刻画和证明命令式程序的合适的框架.
关键词
操作语义
类型
理论
类型系统
程序验证
Keywords
operational semantics
type theory
type system
program verification
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
一种基于扩展Spi演算的类型系统
18
作者
袁霖
王亚弟
韩继红
机构
解放军信息工程大学电子技术学院
出处
《计算机工程与应用》
CSCD
北大核心
2007年第3期131-134,138,共5页
文摘
主要探讨了使用非形式化的原理和形式化的规则来获得密码协议安全属性的方法。这些原理和规则基于传统的等级和信息流的思想,通过将其扩展后用来处理密码协议中的并发进程。提出的规则是基于Spi演算扩展语法的一种类型规则。通过这些规则可以向用户担保,如果协议通过了类型检测,则该协议没有泄漏任何秘密的消息。
关键词
类型系统
密码协议
保密性
类型
规则
Keywords
type system
cryptographic protocols
secrecy properties
typing rules
分类号
TP393 [自动化与计算机技术—计算机应用技术]
下载PDF
职称材料
题名
基于类型理论的XML类型系统形式化建模
19
作者
冯玉才
刘丹
班鹏新
机构
华中科技大学计算机学院
出处
《计算机工程》
EI
CAS
CSCD
北大核心
2004年第12期45-47,共3页
基金
国家"863"计划基金资助项目(2002AA423110)
文摘
利用形式化模型的形式简洁、描述清晰、逻辑性强、易于扩展以及实用性强等优点,运用基于类型理论的逻辑化形式建模技术对XML类型系统进行了形式化建模,实现了对各种XML数据的类型定义和对XML数据处理过程的类型检验,为可直接存储和检索XML数据的XML数据库DM4提供了一种有效的类型系统设计方案。
关键词
XML数据库
XML
类型系统
类型
理论
逻辑化形式建模
Keywords
XMLDB
XML type system
Type theory
Logical formalism modeling
分类号
TP311.13 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
TTCN-3类型系统测试用例集自动生成
20
作者
蒋凡
金鑫
吴文娟
机构
中国科学技术大学计算机科学与技术系
出处
《计算机系统应用》
2009年第9期45-49,共5页
文摘
针对编译器测试中最为重要的测试用例集构造问题,提出了针对TTCN-3语言类型系统的编译器测试用例集层次化、结构化的自动生成方案。语法方面,严格遵从语言规格说明中的扩展巴科斯-瑙尔范式(EBNF);语义正确性上,采用定义"元素定义偏序文件"、建立抽象语法树等多种方法加以保证。实验表明新方案极大提高了测试用例集的生成效率,对TTCN-3类型系统语法、语义两方面都达到很好的测试覆盖,增强了发现编译器缺陷的能力。该方案对于其他语言的编译器测试也具有参考价值。
关键词
TTCN-3
类型系统
编译器测试
测试用例集自动生成
层次化
结构化方法
分类号
TP311.52 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
安全类型系统在编译技术中的应用研究
赵秀凤
杨丽娜
郭渊博
《计算机工程与科学》
CSCD
2008
0
下载PDF
职称材料
2
类型系统的构造、实现及其在程序设计语言中的应用
蒋慧
张兴元
王元元
谢希仁
《南京大学学报(自然科学版)》
CAS
CSCD
北大核心
2001
3
下载PDF
职称材料
3
类型系统λω×≤的范畴论模型
周晓聪
李文军
李师贤
《计算机研究与发展》
EI
CSCD
北大核心
2002
4
下载PDF
职称材料
4
类型系统λω×≤
周晓聪
李文军
李师贤
《中山大学学报(自然科学版)》
CAS
CSCD
北大核心
2001
3
下载PDF
职称材料
5
类型系统λω×≤的PER模型
周晓聪
李文军
李师贤
《计算机研究与发展》
EI
CSCD
北大核心
2000
3
下载PDF
职称材料
6
Gdel语言类型系统
王炳波
赵致琢
晏松
《计算机工程与设计》
CSCD
北大核心
2005
3
下载PDF
职称材料
7
类型系统与程序正确性问题
丁志义
宋国新
邵志清
《计算机科学》
CSCD
北大核心
2006
3
下载PDF
职称材料
8
类型系统的研究与进展
周晓聪
李文军
李师贤
《计算机科学》
CSCD
北大核心
2000
2
下载PDF
职称材料
9
基于类型系统的元数据模型
陈睿
蔡希尧
《软件学报》
EI
CSCD
北大核心
1995
4
下载PDF
职称材料
10
一种带约束的多态类型系统
郑红军
张乃孝
《计算机学报》
EI
CSCD
北大核心
1999
3
下载PDF
职称材料
11
对象在类型系统λω×≤中的表示
周晓聪
李文军
李师贤
《计算机研究与发展》
EI
CSCD
北大核心
2003
1
下载PDF
职称材料
12
建立保护区经营类型系统促进我国保护区事业的发展
刘东来
《林业科学》
EI
CAS
CSCD
北大核心
1996
4
下载PDF
职称材料
13
类型系统的λω×_≤等式理论及其语义的合理性
周晓聪
《计算机研究与发展》
EI
CSCD
北大核心
2006
2
下载PDF
职称材料
14
为π演算建立具有安全级别的简单类型系统(英文)
王立斌
陈克非
《中国科学院研究生院学报》
CAS
CSCD
2002
1
下载PDF
职称材料
15
基于类型系统的完整性信息流控制
王立斌
《华南师范大学学报(自然科学版)》
CAS
2006
1
下载PDF
职称材料
16
面向对象程序设计语言的类型系统
李晓燕
李斌
《小型微型计算机系统》
EI
CSCD
北大核心
2000
1
下载PDF
职称材料
17
命令的操作语义在类型系统中的一种表示
丁志义
宋国新
邵志清
《小型微型计算机系统》
CSCD
北大核心
2006
0
下载PDF
职称材料
18
一种基于扩展Spi演算的类型系统
袁霖
王亚弟
韩继红
《计算机工程与应用》
CSCD
北大核心
2007
0
下载PDF
职称材料
19
基于类型理论的XML类型系统形式化建模
冯玉才
刘丹
班鹏新
《计算机工程》
EI
CAS
CSCD
北大核心
2004
0
下载PDF
职称材料
20
TTCN-3类型系统测试用例集自动生成
蒋凡
金鑫
吴文娟
《计算机系统应用》
2009
0
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
2
…
16
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部