计算机科学 ›› 2006, Vol. 33 ›› Issue (1): 141-143.
• • 上一篇 下一篇
出版日期:
发布日期:
基金资助:
Online:
Published:
摘要： 类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统，因而类型系统可以表迭程序的性质，并自动进行验证。
关键词: 类型系统 程序验证 λ演算 证明理论 程序正确性 语义错误 执行程序 直觉主义 子类型 代码
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
Key words: Type system, Program verification, λ-calculus, Proof theory
. 类型系统与程序正确性问题[J]. 计算机科学, 2006, 33(1): 141-143. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2006/V33/I1/141
Cited
首页