文献类型：期刊文献

中文题名：类型系统与程序正确性问题

英文题名：Type Systems and the Correctness of Program

作者：丁志义[1];宋国新[1];邵志清[1]

机构：[1]华东理工大学计算机科学与工程系

年份：2006

卷号：33

期号：1

起止页码：141

中文期刊名：计算机科学

外文期刊名：Computer Science

收录：CSTPCD;;北大核心:【北大核心2004】；CSCD:【CSCD2011_2012】；

基金：本文工作得到国家自然科学基金和中科院计算机科学重点实验室资助(编号:60373075;SYSKF0305)。

语种：中文

中文关键词：类型系统;程序验证;λ演算;证明理论;程序正确性;语义错误;执行程序;直觉主义;子类型;代码

外文关键词：Type system, Program verification, λ-calculus, Proof theory

摘要：类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统，因而类型系统可以表迭程序的性质，并自动进行验证。
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 theory. The base of the theory is the typed λ-calculus. Higher-order type system of higher-order subtyping, known as F^w≤, has been used as a core calculus for typed languages. The Curry-Howard isomorphism is a correspondence between type systems and intuitionistic logic. Proof generation capabilities of proof construction systems are based on type theory. Type systems allow us to express program properties that are automatically verified.