Semantics of constructions (II) — The initial algebraic approach
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.
Keywordstype theory inductive type ω-set T-algebra
Unable to display preview. Download preview PDF.
- 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
- 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
- Coquand T, Paulin-Mohring C. Inductively Defined Types. InCOLOG’88, Lecture Notes in Computer Science 417, Springer-Verlag, 1990, pp.50–66.Google Scholar