| 基于类型理论的递旧元程序设计 |
| |
| 引用本文： | 谭庆平,陈火旺. 基于类型理论的递旧元程序设计[J]. 软件学报, 1994, 5(8): 30-36 |
| |
| 作者姓名： | 谭庆平 陈火旺 |
| |
| 作者单位： | 长沙工学院计算机科学系，长沙 410073;长沙工学院计算机科学系，长沙 410073 |
| |
| 摘 要： | 本文提出在ＬＦ类型理论中定义一组相互递归类型的方法，并对递归类型赋予操作语义．这样，递归类型不仅可以表示通常的递归数据结构，还可描述一般的递归问题求解、递归证明构造和递归程序构造过程．
|
| 关 键 词： | 类型理论，证明开发环境，递归 |
| 收稿时间： | 1991-05-05 |
| 修稿时间： | 1992-05-11 |
RECURSIVE METAPROGRAMMING BASED ON TYPE THEORY |
| |
| Tan Qingping and Chen Huowang. RECURSIVE METAPROGRAMMING BASED ON TYPE THEORY[J]. Journal of Software, 1994, 5(8): 30-36 |
| |
| Authors: | Tan Qingping and Chen Huowang |
| |
| Abstract: | This paper presents a new approach to defining a set of mutually inductivetypes and gives these types an operational interpretation. Therefore, inductive types canexpress ordinary inductive data structures as well as recursive problem solving and proofcons truction. |
| |
| Keywords: | Type theory proof development environment recursive. |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载免费的PDF全文 |
