| Item type |
Symposium(1) |
| 公開日 |
2015-01-09 |
| タイトル |
|
|
タイトル |
Agdaによる型推論器の定式化 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Type Inference in Agda |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
Agda, Type Inference, Proof Theory |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_5794 |
|
資源タイプ |
conference paper |
| 著者所属 |
|
|
|
お茶の水女子大学 |
| 著者所属 |
|
|
|
お茶の水女子大学 |
| 著者所属(英) |
|
|
|
en |
|
|
Ochanomizu University |
| 著者所属(英) |
|
|
|
en |
|
|
Ochanomizu University |
| 著者名 |
門脇, 香子
浅井, 健一
|
| 著者名(英) |
Kyoko, Kadowaki
Kenichi, Asai
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
Agda はマルティンレフの型理論に基づいた定理証明支援器であり,その一方で依存型をもつ関数型プログラミング言語でもある.Agda では依存型 (Dependant Types) を用いることができるのも大きな特徴である.また,定理証明支援器とプログラミング言語両方の特徴をもちあわせていることから,何かを実装しつつ証明するのに適している.そこで本稿では,停止性が保証された型推論器を Agda により構成する.なかでも, Unification の実装では, McBride の手法を採用する.これは型変数の数を巧妙に管理することで構造に従った再帰を使って(つまり停止性が明らかな形で)型の Unification を表現できることを示したものである.本稿では Term の型変数の数に注目しつつ,主に Unification の部分と Application の実装にフォーカスを当てながら実装していく. |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
Agda is a dependently typed functional programming language based on Zhaohui Luo's UTT a type theory similar to Martin-L‡f type theory. Agda is also based on dependent type theory.This paper used Agda to implement a Type inference guaranteed to avoid compose non-stopping program by a structural recursion of McBride's technique. This paper focused number of typing variables, Unification and implementation of application data constructor. |
| 書誌情報 |
第56回プログラミング･シンポジウム予稿集
巻 2015,
p. 115-120,
発行日 2015-01-09
|
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-WPRO2015020.pdf (270.2 kB)
