Constructive Semantics of Inductive Types
归纳类型的构造集语义

Inductive types in Martin-Lof type theory have simple interpretations in classical set theory. The calculus of constructions however does not enjoy such a model. This paper shows how inductive types in the calculus of constructions can be interpreted in the category of omega sets.