Journal of Computer Science and Technology

, Volume 16, Issue 2, pp 137–145 | Cite as

Semantics of constructions (II) — The initial algebraic approach

  • Fu Yuxi 


Inductive types can be formulated by incorporating the idea of initialT-algebra. The interpretation of an inductive type of this kind boils down to finding out the initialT-algebra defined by the inductive type. In this paper the issue in the semantic domain of omega sets is examined. Based on the semantic results, a new class of inductive types, that of local inductive types, is proposed.


type theory inductive type ω-set T-algebra 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Nordström B, Petersson K, Smith J. Programming in Martin-Löf’s type theory — An introduction. InInternational Series of Monographs on Computer Science 7, Oxford University Press, 1990.Google Scholar
  2. [2]
    Coquand T, Huet G. The calculus of constructions.Information and Computation, 1998, 76(1): 95–120.MathSciNetGoogle Scholar
  3. [3]
    Fu Y. Semantics of constructions (I) — The traditional approach.Journal of Computer Science and Technology, 2001, 16(1): 13–24.MATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    Ore C. The extended calculus of constructions (ECC) with inductive types.Information and Computation, 1992, 99(1): 231–264.MATHCrossRefMathSciNetGoogle Scholar
  5. [5]
    Hagino S. A typed lambda calculus with categorical type constructions. InCategory Theory in Computer Science, Lecture Notes in Computer Science 283, Springer, 1987, pp.140–157.Google Scholar
  6. [6]
    Adámek J, Koubek V. Least fixed point of a functor.Journal of Computer Systems, 1979, 19(1): 163–178.MATHCrossRefGoogle Scholar
  7. [7]
    Coquand T, Paulin-Mohring C. Inductively Defined Types. InCOLOG’88, Lecture Notes in Computer Science 417, Springer-Verlag, 1990, pp.50–66.Google Scholar

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 2001

Authors and Affiliations

  1. 1.Department of Computer ScienceShanghai Jiao Tong UniversityShanghaiP.R. China

Personalised recommendations