计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2006年
1期
141-143,157
,共4页
类型系统%程序验证%λ演算%证明理论
類型繫統%程序驗證%λ縯算%證明理論
류형계통%정서험증%λ연산%증명이론
类型系统能检出合法程序的语义错误,可以缩短调试时间,在执行程序之前捕获代码中的错误.类型系统的理论基础是类型化的λ演算.带子类型的高阶类型系统Fw≤已成为类型化语言的演算核心[5].类型系统和直觉主义极小逻辑是同构的.证明系统的能力取决于类型系统,因而类型系统可以表达程序的性质,并自动进行验证.
類型繫統能檢齣閤法程序的語義錯誤,可以縮短調試時間,在執行程序之前捕穫代碼中的錯誤.類型繫統的理論基礎是類型化的λ縯算.帶子類型的高階類型繫統Fw≤已成為類型化語言的縯算覈心[5].類型繫統和直覺主義極小邏輯是同構的.證明繫統的能力取決于類型繫統,因而類型繫統可以錶達程序的性質,併自動進行驗證.
류형계통능검출합법정서적어의착오,가이축단조시시간,재집행정서지전포획대마중적착오.류형계통적이론기출시류형화적λ연산.대자류형적고계류형계통Fw≤이성위류형화어언적연산핵심[5].류형계통화직각주의겁소라집시동구적.증명계통적능력취결우류형계통,인이류형계통가이표체정서적성질,병자동진행험증.
