2017 Fiscal Year Annual Research Report
Design and development of multi-stage languages for verification
| Project/Area Number |
15K12007
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 定理証明支援システム / メタプログラミング / プログラム抽出・生成 / 型システム / 型安全性 / スコープ安全性 |
|---|
| Outline of Annual Research Achievements |
マルチステージ記述言語の設計・実装のため、マルチステージプログラミング言語MetaOCamlとそれに基づく証明記述言語を中心とした研究を行い、以下の成果を得た。
（1）前年度の成果である「let挿入」技術について、挿入先のポイントが複数あっても安全なコードを生成できる言語と型システムを作成するとともに論文を完成させ、IFIP Working Groupおよび Generative Programming and Component Softwareに関する国際会議で研究発表を行った。これらの会議では複雑なコード生成を行う様々なアプローチについての研究発表が行われ、それらとの比較検討の上で、本研究の有利な点を明確化することができた。
（2）モジュール抽象はOCaml言語で大規模プログラミングを書いたり、Coqで大規模証明を書いたりする場合には不可欠の機能である。一方、現在のコード生成言語ではモジュールを生成するプログラムにおける安全性はほとんど議論されていない。Inoueらの先行研究では、モジュールのコードを生成する言語が有益な応用先が示されているが、そのような言語設計は未解決問題とされていた。そこで、モジュールを安全に生成することを可能とする言語および型システムについての研究を行った。その結果、２レベルに限定した範囲ながら、モジュールのコードを生成できる型安全な言語を設計することができ、さらに、この言語から既存のMetaOCaml言語へのプログラム変換を定義することができた。さらに、後者の型安全性を保証することができ、先行研究において未解決とされていた問題を、（２レベルの範囲では）解決することができた。この成果は、言語設計と変換を実装しており、実際に使える言語となっている。
これらの成果によりマルチステージ証明記述言語において鍵となる要素技術について解決を果たした。
|
Research Products
(6 results)
