%0 Journal Article
%T 类型系统与程序正确性问题
%J 计算机科学
%D 2006
%X 类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统，因而类型系统可以表迭程序的性质，并自动进行验证。
%K 类型系统程序验证λ演算证明理论程序正确性语义错误执行程序直觉主义子类型代码
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=21101840&flag=1