基于类型理论的递旧元程序设计  

RECURSIVE METAPROGRAMMING BASED ON TYPE THEORY

作　　者：谭庆平[1] 陈火旺[1] 

机构地区：[1]长沙工学院计算机科学系

出　　处：《软件学报》1994年第8期30-35,共6页Journal of Software

摘　　要：本文提出在ＬＦ类型理论中定义一组相互递归类型的方法，并对递归类型赋予操作语义．这样，递归类型不仅可以表示通常的递归数据结构，还可描述一般的递归问题求解、递归证明构造和递归程序构造过程．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.

关 键 词：类型理论 递归 程序设计 数据结构 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]