2012 Fiscal Year Annual Research Report
進んだ型システムを持ったプログラミング言語における型検証器の機械的な証明
| Project/Area Number |
22700028
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Project Period (FY) |
2010-04-01 – 2014-03-31
|
| Keywords | プログラミング言語論 / プログラムパラダイム / 定理証明支援系 |
|---|
| Research Abstract |
この一年では、副作用を考慮した多相性の制限を実装し、その健全性もCoqで証明した。OCamlで採用されている「緩和された値限定多相性」は通常のML系言語に比べて柔軟性があるが、その証明が「意味的な型」を利用するのが特徴的である。フランスから修士課程の研修で来たENS LyonのThomas Leventis氏と一緒に証明方針を考え、それをCoqに移した。途中結果として、その理論的な基礎であるFrancois Pottierが提案したBT(X)という型体系の健全性の証明も得られた。ただ、証明方針がもとのインタープリターと異なっているので、これからその結果を組み込む方法を考えなければならない。
また、タリン工科大学の中田景子氏と一緒に、再帰型定義の整礎性・正則性を確認するアルゴリズムの形式化を始めた。具体的には、メモリ・グラフの上で定義されているOCamlのアルゴリズムをCoqで明示的なグラフ構造で実装し、証明を始めた。現時点では型の完全な展開の停止性および展開がグラフの性質を崩さないことが証明されている。これから、グラフの意味が変わらないことと、正則性のチェックに関する証明を完成させなければならない。
このCoqでの証明と並行して、OCamlの型システムの拡張が続いている。2012年7月にGADT(一般化代数的データ型)を含んだOCaml 4.00がリリースされた、そこではフランスのINRIAのDidier Remyと一緒に考えた集合の単一化による曖昧性の解消法が採用されている。それについてCopenhagenのML Workshopで発表したが、最近になって具体的な証明が完成したので、近々論文を投稿する予定である。
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
研究実績の概要に書いてあるとおり、様々な機能の証明が着実に進んでいる。しかし、もとの方針では、機能を次々とコア言語に追加する予定であったが、現時点では証明を独立に行っている。もとの方針に従って実装すると、相乗効果で証明が複雑になり、新たに機能を追加する際の壁が段々高くなる。そのために、そういうことの起きない証明の構造を考えなければならない。
|
| Strategy for Future Research Activity |
研究実績の概要や現在までの達成度に書いたように、今までの方法で次々と新しい機能を追加して行くのはかなりの労力を必要とする。モジュラリティの高いやり方を考えながら、各機能を別々で証明して行く形で進めるつもりである。最終的には全ての部分をまとめて一つの型検証器を作らなければならないが、それぞれの部分に対して新しい試みができ、より良い方法が見つかる可能性がある。
|
