-
题名构造类型论与计算机程序设计
被引量：1
- 1
-
-
作者
蒋慧
林东
孙泉
谢希仁
-
机构
解放军理工大学计算机系
国防大学军队指挥学博士后流动站
北京大学计算机系
-
出处
《计算机科学》
CSCD
北大核心
2002年第2期72-77,61,共7页
-
基金
国家自然科学基金69931040
国防科研基金GF00J6.2.1.JB0501
-
文摘
1.引言近些年来,在计算机程序设计语言理论、自动演绎以及更一般的逻辑和计算领域研究中,出现了多种以构造类型论为基础的系统,如LCF、ALF、LEGO、Coq等,它们被用来为程序设计语言设计类型系统,进行程序开发和验证、形式化证明以及作为数学和计算的基础.构造类型论为计算机科学家提供了一个框架,以一种优雅和灵活的方式把逻辑和程序设计语言结合起来:在同一形式系统中,可以同时表达规约和(函数式语言)程序,从证明规则可以导出正确的程序,并验证程序具有某种性质,从而在同一系统内完成程序的开发和验证[26,19].
-
关键词
限制谓词演算
构造类型论
构造数学
计算机
程序设计
程序设计语言
-
Keywords
Constructive type theory,Type theory, Intuitionistic logic, Automated deduction, Lambda calculus, Proof theory
-
分类号
O141
[理学—数学]
TP311.1
[理学—基础数学]
-
