研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	英語
発行・発表の年月	2002
形態種別	学術雑誌
査読	査読あり
標題	An implementation of Type:Type
執筆形態	共著
掲載誌名	Types for Proofs and Programs 2000, Lecture Notes in Computer Science, vol.2277
掲載区分	国外
巻・号・頁	2227,pp.53-62
著者・共著者	Thierry Coquand, Makoto Takeyama
概要	We present a denotational semantics of a type system with dependent types, where types are interpreted as finitary projections. We prove then the correctness of a type-checking algrithm w.r.t. this semantics. In this way, we can justify some simple optimisation in this algorithm. We then sketch how to extend this semantics to allow a simple record mechanism with manifest fields.