类型系统与程序正确性问题

摘要：

类型系统能检出合法程序的语义错误,可以缩短调试时间,在执行程序之前捕获代码中的错误.类型系统的理论基础是类型化的λ演算.带子类型的高阶类型系统Fw≤已成为类型化语言的演算核心[5].类型系统和直觉主义极小逻辑是同构的.证明系统的能力取决于类型系统,因而类型系统可以表达程序的性质,并自动进行验证.

关键词：类型系统、程序验证、λ演算、证明理论

所属期刊栏目：33

分类号：TP3(计算技术、计算机技术)

资助基金：中国科学院资助项目;中国科学院重点实验室基金60373075;SYSKF0305

在线出版日期：2006-03-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：141-143,157