归纳证明在类型理论中的应用研究

• 作者: 袁晓月 黎爽
• 来源期刊: 江西科学
• 关键词: 归纳法 类型理论 类型性质证明
• 年，卷（期）: 2015,（2）
• 所属期刊栏目: 信息科学
• 页码范围: 248-253
• 页数: 6页
• 分类号: TP301.2
• 语种: 中文
• DOI: 10.13990/j.issn1001-3679.2015.02.025

摘要

通过类型理论使得程序语言在静态可以检查是否出错,这给程序语言带来许多优势.类型理论中的重要性质包括:弱化规则、删除规则、强化规则等.首先给出了结构归纳法、良基归纳法、规则归纳法和余归纳法的形式化定义.在给出PA4WS进程代数的语法、语义的基础上给出了其类型定义.在此基础上给出了归纳法在PA4WS类型理论性质证明的应用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	袁晓月	江西省科学院应用物理研究所	13	17	2.0	3.0
2	黎爽	江西财经大学信息管理学院	1	0	0.0	0.0