中文摘要：

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

英文摘要：

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.