命令的操作语义在类型系统中的一种表示  

Imperative Operational Semantics in Type Theory

作　　者：丁志义[1] 宋国新[1] 邵志清[1] 

机构地区：[1]华东理工大学计算机科学与工程系

出　　处：《小型微型计算机系统》2006年第7期1285-1288,共4页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60373075)资助;教育部科学技术研究重点项目(01077)资助;中科院计算机科学重点实验室项目(SYSKF0305)资助;上海市科学技术委员会科研计划项目(045115006)资助.

摘　　要：类型系统建立在一个小的规则集合基础上,易于实现,可理解性好,且具有计算完全性和足够的表达能力.在类型系统中可以重述推导规则,将其形式化为一些归纳关系,从而直接表示了命令的操作语义.类型理论不仅适合于函数式程序的证明,也是刻画和证明命令式程序的合适的框架.Type theory provides expressive and sound logics, which are well understooa and relatively easy to be implementod since they are based on a small set of rules. The goal in this paper is to develop operational semantics in pure type systems. It is a straightforward implementation, the derivation system is formalized as inductive relations by directly describing the derivation rules. Type theory is naturally well-suited for the proof of purely functional programs. It can be shown that type system is also a good framework to specify and prove imperative programs.

关 键 词：操作语义 类型理论 类型系统 程序验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]