作者：丁志义; 宋国新; 邵志清类型系统程序验证证明理论程序正确性语义错误执行程序直觉主义子类型代码
摘要：类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统，因而类型系统可以表迭程序的性质，并自动进行验证。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《计算机科学》（CN：50-1075/TP）是一本有较高学术价值的大型月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《计算机科学》报导国内外计算机科学与技术的发展动态，以其新颖、准确、及时为特色，突出动态性、综述性、学术性，“前沿学科”与“基础研究”相结合；“优秀技术”与“支撑技术”相结合；“倡导”与“争鸣”相结合。
省级期刊
人气 753873 评论 72
人气 484721 评论 71
人气 464634 评论 66
部级期刊
人气 442109 评论 69
