研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	日本語
発行・発表の年月	2009
形態種別	学術雑誌
標題	Agate－an Agda-to-Haskell compiler
執筆形態	共著
掲載誌名	コンピュータソフトウェア　26-4
巻・号・頁	26(4),107-119頁
著者・共著者	Hiroyuki Ozaki, Makoto Takeyama, Yosiki Kinoshita
概要	We report some features of Agate, a compiler for the dependently typed functional language of the Agda proof-assistant. Agate was developed as an experimental platform for the practice of dependently typed programming and extends the Agda language with I/O facilities and calls to Haskell functions. The first feature is the use of Higher-Order Abstract Syntax to translate terms of the Agda language into untyped λ-calculus encoded in Haskell. The second feature is the application of the Haskell class mechanism to embed typed Haskell terms in the universal type for untyped λ-calculus. This approach makes Agate very lightweight. The performance of a number of codes generated by Agate is evaluated.