摘要
1.引言近些年来,在计算机程序设计语言理论、自动演绎以及更一般的逻辑和计算领域研究中,出现了多种以构造类型论为基础的系统,如LCF、ALF、LEGO、Coq等,它们被用来为程序设计语言设计类型系统,进行程序开发和验证、形式化证明以及作为数学和计算的基础.构造类型论为计算机科学家提供了一个框架,以一种优雅和灵活的方式把逻辑和程序设计语言结合起来:在同一形式系统中,可以同时表达规约和(函数式语言)程序,从证明规则可以导出正确的程序,并验证程序具有某种性质,从而在同一系统内完成程序的开发和验证[26,19].
Recent years, in the area of computer programming language theories, automated deduction, and more generalized area of logic and computing, a lot of systems based on constructive type theory are used widely to design type system for computer programming languages, to do formal system development and verification, and to be used as foundation of mathematics and computing. Constructive type theory provides computer scientists with a framework to combine logic and computer program design in an elegant and flexible way. In this paper, the evolvement of constructive type theory is first introduced. The several foundations of type theory are then discussed, together with analysis of the relationships between them. The relation between constructive type theory and computer programming is explored in-depth. In the last, Martin Lof's intuitionistic type theory is used as an example to demonstrate how to do program development and verification in the same formal system.
出处
《计算机科学》
CSCD
北大核心
2002年第2期72-77,61,共7页
Computer Science
基金
国家自然科学基金69931040
国防科研基金GF00J6.2.1.JB0501
关键词
限制谓词演算
构造类型论
构造数学
计算机
程序设计
程序设计语言
Constructive type theory,Type theory, Intuitionistic logic, Automated deduction, Lambda calculus, Proof theory