研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	英語
発行・発表の年月	2005/02
形態種別	学術雑誌
査読	査読あり
標題	A Logical Framework with Dependently Typed Records
執筆形態	共著
掲載誌名	Fundamenta Informaticae,vol.65(1-2)
巻・号・頁	65(1-2),pp.113-134
著者・共著者	Thierry Coquand, Randy Pollack, Makoto Takeyama
概要	Our long term goal is a system to formally represent complex structured mathematical objects, and proofs and computation on such objects; e.g. a foundational computer algebra system. Our approach is informed by the long development of module systems for functional programming based on dependent record types as signatures. For our logical purposes, however, we want a dependently typed base language. In this paper we propose an extension of Martin-Lof's logical framework with dependently typed records, and present the semantic foundation and the typechecking algorithm of our system. Some of the work is formally checked in Coq. We have also implemented and experimented with several related systems. Our proposal combines a semantic foundation, provably sound typechecking, good expressiveness (e.g. subtyping, sharing) and first-class higher-order modules.