研究者情報 | 神奈川大学

キノシタ　ヨシキ Kinoshita Yoshiki 木下　佳樹所属神奈川大学情報学部計算機科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	日本語
発行・発表の年月	2009/09
形態種別	著書
査読	査読あり
標題	A simple type-theoretic language: Mini-TT
執筆形態	共著
出版社・発行元	In "From Semantics Computer Science" (eds. Y. Bertot, G. Huet, J.-J. Levy and G. Plotkin) (Cambridge University Press)
巻・号・頁	139-164頁
著者・共著者	Thierry Coquand, Yoshiki Kinoshita, Bengt Nordstrom and Makoto Takeyama
概要	This paper presents a formal description of a small functional language with dependent types. The language contains data types, mutual recursive/inductive definitions and a universe of small types. The syntax, semantics and type system is specified in such a way that the implementation of a parser, interpreter and type checker is straightforward. The main difficulty is to design the conversion algorithm in such a way that it works for open expressions. The paper ends with a complete implementation in Haskell (around 400 lines of code).