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

Imperative Operational Semantics in Type Theory

类型系统建立在一个小的规则集合基础上,易于实现,可理解性好,且具有计算完全性和足够的表达能力.在类型系统中可以重述推导规则,将其形式化为一些归纳关系,从而直接表示了命令的操作语义.类型理论不仅适合于函数式程序的证明,也是刻画和证明命令式程序的合适的框架.

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.