| 命令的操作语义在类型系统中的一种表示 |
| |
| 引用本文： | 丁志义,宋国新,邵志清.命令的操作语义在类型系统中的一种表示[J].小型微型计算机系统,2006,27(7):1285-1288. |
| |
| 作者姓名： | 丁志义 宋国新 邵志清 |
| |
| 作者单位： | 1. 华东理工大学,计算机科学与工程系,上海,200237;宁夏大学,数学计算机学院,宁夏,银川,750021
2. 华东理工大学,计算机科学与工程系,上海,200237 |
| |
| 基金项目： | 国家高技术研究发展计划(863计划);教育部科学技术研究项目;中国科学院重点实验室基金;上海市科委资助项目 |
| |
| 摘 要： | 类型系统建立在一个小的规则集合基础上，易于实现，可理解性好，且具有计算完全性和足够的表达能力,在类型系统中可以重述推导规则，将其形式化为一些归纳关系，从而直接表示了命令的操作语义,类型理论不仅适合于函数式程序的证明，也是刻画和证明命令式程序的合适的框架。
|
| 关 键 词： | 操作语义 类型理论 类型系统 程序验证 |
| 文章编号： | 1000-1220（2006）07-1285-04 |
| 收稿时间： | 04 13 2005 12:00AM |
| 修稿时间： | 2005-04-13 |
Imperative Operational Semantics in Type Theory |
| |
| DING Zhi-yi,SONG Guo-xin,SHAO Zhi-qing.Imperative Operational Semantics in Type Theory[J].Mini-micro Systems,2006,27(7):1285-1288. |
| |
| Authors: | DING Zhi-yi SONG Guo-xin SHAO Zhi-qing |
| |
| Affiliation: | 1.Department of Computer Science and Engineering, East China University of Science and Technology, Shanghai 200237, China;2.School of Mathematics and Computer Science, Ningxia University, Yinchuan 750021, China |
| |
| Abstract: | 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. |
| |
| Keywords: | operational semantics type theory type system program verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
