| 类型系统与程序正确性问题 |
| |
| 引用本文： | 丁志义,宋国新,邵志清. 类型系统与程序正确性问题[J]. 计算机科学, 2006, 33(1): 141-143 |
| |
| 作者姓名： | 丁志义 宋国新 邵志清 |
| |
| 作者单位： | 华东理工大学计算机科学与工程系,上海,200237;宁夏大学数学计算机学院,银川,750021;华东理工大学计算机科学与工程系,上海,200237 |
| |
| 基金项目： | 中国科学院资助项目;中国科学院重点实验室基金 |
| |
| 摘 要： | 类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统，因而类型系统可以表迭程序的性质，并自动进行验证。
|
| 关 键 词： | 类型系统 程序验证 λ演算 证明理论 |
Type Systems and the Correctness of Program |
| |
| DING Zhi-Yi,SONG Guo-Xin,SHAO Zhi-Qing. Type Systems and the Correctness of Program[J]. Computer Science, 2006, 33(1): 141-143 |
| |
| Authors: | DING Zhi-Yi SONG Guo-Xin SHAO Zhi-Qing |
| |
| Affiliation: | 1.Department of Computer Science and Engineering, East China University of Science and Technology, Shanghai 200237;2.Institute of Mathematics and Computer Science, Ningxia University, Yinchuan 750021 |
| |
| Abstract: | When type systems detect legitimate program errors, they help to reduce the time spent debugging. Type systems catch errors in code that is not executed by the programmer. Proof generation capabilities of proof construction systems are based on type theor |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
