Agda による型推論器の定式化2. http://github.com/KDXU/InferAgda 研究概要 • Agda を用いて停止性と正当性がそれぞれ保証され た型推論器を pure functional に実装した • unification の実装部分は McBride の手法を採用 した • 主に unification の部分と application の実装に フォーカスを当てながら解説します • コード : http://github.com/KDXU/InferAgda 2 3. http://github.com/KDXU/InferAgda Agdaについて • 依存型を用いた，Haskell に似た構文をもつ定理 証明支援系言語 • プログラミング言語と定理証明支援系言語の両面 を持っている → 何かを実装しつつ証明をするのに適している • マルティンレフの型理論に基づいている 3
