We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 12 Issue 3
May  1997
Turn off MathJax
Article Contents
Abstract
References
Tan Qingping. A Higher-Order Unification Algorithm for Inductive Types and Dependent Types[J]. Journal of Computer Science and Technology, 1997, 12(3): 231-243.
Citation: Tan Qingping. A Higher-Order Unification Algorithm for Inductive Types and Dependent Types[J]. Journal of Computer Science and Technology, 1997, 12(3): 231-243.
shu

A Higher-Order Unification Algorithm for Inductive Types and Dependent Types

  • Department of Computer Science; Changsha Institute of Technology; Changsha 410073;

More Information
  • Published Date: May 09, 1997
    Abstract
  • This paper presents a method to define a set of mutuaJly recursive inductive types, and develops a higherorder unilication algorithm for Anz extended with inductive types. The algorithm is an extension of Eiliott's algoritbJn for λ∑.The notation of normal forms plays a vital role in higher-order unification.The weak head normal forms in the extended troe theory is defined to reveal the ultimate "top level structures" of the fully normalized terms and types. Unification transformation rules are designed to deal with inductive types, a recursive operator and its reduction rule. The algoritlun can construct recuxsive functions automatically.
    • FullText(HTML)
    • References (3)
  • [1]
    Elliott C. Extensions and applications of higher-order unification. Ph.D. Thesis, Carnegie Mellon University, 1990.
    [2]
    Tan Qingping. Program design environments based on type theory. Ph.D. Thesis, Changsha Institute of Technology, 1992.
    [3]
    Huet G. A unification algorithm for typed a-calculus. Theor. Comput. Sci.,1975, 1. ………..
    • Relative Articles
  • Supplements (0)

Catalog

    Get Citation
    PDF
    XML
    Article views (24) PDF downloads (1295) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return