| 研究課題/領域番号 |
15K12007
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 定理証明支援システム / メタプログラミング / プログラム抽出・生成 / 型システム / 型安全性 / スコープ安全性 |
|---|
| 研究実績の概要 |
マルチステージ記述言語の設計・実装のため、定理証明支援システムCoqおよびマルチステージプログラミング言語MetaOCamlを中心とした研究を行い、以下の成果を得た。
（１）Coqの有限ドメイン関数ライブラリを使った証明から抽出したプログラムの効率をあげるための研究をさらに進めて、改善したライブラリを構築し、17万行におよぶ有限位数定理の証明について、わずか8行の変更で対応できるなど、従来の証明資産を受け継いだ形でライブラリの置き換えが可能であること、したがって、このライブラリが非常に広い範囲で適用できることを示した。また、行列乗算や算術体系の充足可能性の決定手続きなどに適用し、大幅に効率が改善することを示した。この成果は情報処理学会のプログラミング研究会および論文誌で発表した。
（２）マルチステージプログラムの信頼性に関する研究として、変数スコープの安全性を型システムにより静的に保証する研究を推進し、従来は扱うことができなかったグローバルな破壊的変数をもつ体系においても安全性が保証できることを理論的に証明するとともに、プロトタイプ実装を与えた。これは、自然演繹体系の固有変数条件をヒントとして設計した体系を拡張した形で与えたものであり、論理学的知見を設計のガイドとして使ったため、見通しの良い設計が可能となった。この研究の成果は、国際会議APLASで発表した。
（３）上記の（２）のテーマに関連する別の研究項目として、コード生成時に発生する部分式を共有する仕組みの１つである「let挿入」という技術について研究を行い、挿入先のポイントが複数ある場合についても安全なコードを生成できる型システムを設計した。この研究成果に関する初期段階のものを日本ソフトウェア科学会大会において発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
マルチステージ証明記述言語の設計と実現に向けて、最も重要な要素技術である定理証明系におけるプログラム抽出機能と、マルチステージプログラミング言語に関する安全性・信頼性に関する技術的に重要な成果を得た。
|
| 今後の研究の推進方策 |
マルチステージ証明記述言語の仕上げとなる研究を行う。平成28年度に得られた重要な成果等を組み合わせて、マルチステージ（多段階）で証明を記述し、高い信頼性をもつ効率の良いプログラムを生成できるようにする。
|
| 次年度使用額が生じた理由 |
今年度はマルチステージ証明記述言語の理論的側面を中心に研究を進めたため、理論的成果は出たが、システムとしての言語実装や実例作成などを中心とした人件費・物件費の発生が当初予定より少なかったため。
|
| 次年度使用額の使用計画 |
最終年度となる平成29年度は、言語実装のための人件費、そのためのパーソナルコンピュータ等の購入、成果を国際会議で発表するための旅費などにより、研究費をすべて使用する予定である。
|
