RECURSIVE METAPROGRAMMING BASED ON TYPE THEORY
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [1]
  • |
  • Related [20]
  • | | |
  • Comments
    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.

    Reference
    1 Coauand T,Paulin C.Inductively defined types.Proc.of International Conf.on Computer Logic,LNCS 417,1988. 2 HarDer R,Honsell F,Plotkin G.A framework for defining logics.Proc.of LICS'87,1987. 3 Pfenning F.Elf:a language for logic definition and verified metaprogramming. PrOC.of LICS'89,1989. 4 谭庆平,徐锡山,陈火旺.证明开发环境中的元语言:设计与实现.全国人工智能与智能计算机学术会议,北京,1991. 5 谭庆平.基于类型理论的程序设计环境.工学博士学位论文,国防科技大学研究生院,1992.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

谭庆平,陈火旺.基于类型理论的递旧元程序设计.软件学报,1994,5(8):30-36

Copy
Share
Article Metrics
  • Abstract:3744
  • PDF: 4472
  • HTML: 0
  • Cited by: 0
History
  • Received:May 05,1991
  • Revised:May 11,1992
You are the first2032791Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063