×

Semantics of constructions. II: The initial algebraic approach. (English) Zbl 0992.68139

[For part I see ibid. 16, No. 1, 13-24 (2001; Zbl 0974.03032).]
Summary: Inductive types can be formulated by incorporating the idea of initial \(T\)-algebra. The interpretation of an inductive type of this kind boils down to finding out the initial \(T\)-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.

MSC:

68Q55 Semantics in the theory of computing

Citations:

Zbl 0974.03032
PDFBibTeX XMLCite
Full Text: DOI

References:

[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. · Zbl 0744.03029
[2] Coquand T, Huet G. The calculus of constructions.Information and Computation, 1998, 76(1): 95–120. · Zbl 0654.03045 · doi:10.1016/0890-5401(88)90005-3
[3] Fu Y. Semantics of constructions (I) – The traditional approach.Journal of Computer Science and Technology, 2001, 16(1): 13–24. · Zbl 0974.03032 · doi:10.1007/BF02948849
[4] Ore C. The extended calculus of constructions (ECC) with inductive types.Information and Computation, 1992, 99(1): 231–264. · Zbl 0784.03009 · doi:10.1016/0890-5401(92)90031-A
[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. · Zbl 0643.03010
[6] Adámek J, Koubek V. Least fixed point of a functor.Journal of Computer Systems, 1979, 19(1): 163–178. · Zbl 0423.18007 · doi:10.1016/0022-0000(79)90026-6
[7] Coquand T, Paulin-Mohring C. Inductively Defined Types. InCOLOG’88, Lecture Notes in Computer Science 417, Springer-Verlag, 1990, pp.50–66.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.