| 摘要: |
| 本文提出在ＬＦ类型理论中定义一组相互递归类型的方法，并对递归类型赋予操作语义．这样，递归类型不仅可以表示通常的递归数据结构，还可描述一般的递归问题求解、递归证明构造和递归程序构造过程． |
| 关键词: 类型理论，证明开发环境，递归 |
| DOI： |
| 分类号: |
| 基金项目: |
|
| RECURSIVE METAPROGRAMMING BASED ON TYPE THEORY |
|
Tan Qingping,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. |
| Key words: Type theory, proof development environment, recursive. |
