%0 Journal Article
%T Constructive Semantics of Inductive Types<br>归纳类型的构造集语义
%A FU Yu-xi
%A <br>傅育熙
%J 软件学报
%D 1998
%I 
%X 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.
%K 类型理论
%K 归纳类型
%K ω-集合.
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=58A248B9D2D4CC9F&yid=8CAA3A429E3EA654&vid=9CF7A0430CBB2DFD&iid=38B194292C032A66&sid=FBCA02DBD05BD4EA&eid=C812B90E96151014&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=16