摘要
类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子类型的高阶类型系统腿已成为类型化语言的演算核心。类型系统和直觉主义极小逻辑是同构的。证明系统的能力取决于类型系统，因而类型系统可以表迭程序的性质，并自动进行验证。
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.
出处
《计算机科学》
CSCD
北大核心
2006年第1期141-143,157,共4页
Computer Science
基金
本文工作得到国家自然科学基金和中科院计算机科学重点实验室资助(编号:60373075
SYSKF0305)。
