2015 Fiscal Year Research-status Report
| Project/Area Number |
15K12013
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田中 哲 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (10357452)
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 定理証明支援系 / 簡潔データ構造 / プログラミング言語OCaml |
|---|
| Outline of Annual Research Achievements |
平成27年度、簡潔データ構造の基礎を形式化し、基礎的なアルゴリズムの形式検証に成功した。まず、定理証明支援系Coqを用いて、簡潔データ構造の基礎となるrank関数などを抽象的に定義し、その性質の証明に取り組み、定理群の開発を開始した。特に、アルゴリズムが利用するメモリ量に関する性質に集中した。また、検証済みで実用的なrank関数を得るため、定理証明支援系Coqを用いた検証方法を提案し、検証実験を行った。簡潔データ構造は低レベルな操作を利用するため、通常の実装の検証は困難である。具体的には、抽象的なrankアルゴリズムを検証してから、CoqのExtraction機能を用いて、OCaml言語の実装を出力した。但し、効率のいいコードが得られるように、ビット列を表現するOCamlライブラリを新しく構築した。特に、このライブラリは最新のIntelアーキテクチャの命令を利用する。以上の実験に関する論文を国内ワークショップに投稿し、採択され、本ワークショップの論文賞を受賞した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成27年度、簡潔データ構造に関する実装はビット列のレベルで実現し、実用的な実装を得たので、本プロジェクトの目的の一つを達成した。
|
| Strategy for Future Research Activity |
平成２７年度の成果を向上し、国際会議に投稿あるいは雑誌論文を作成する。平成２７年度に提案した検証方法を簡潔データ構造のselectアルゴリズムに適用する。提案した定理群を拡張あるいは整理と拡張する。MathCompの実数を利用できるように移植する。簡潔木の形式化を開始する。
|
| Causes of Carryover |
名古屋で会議を行わなかったので、未使用額が生じた。計画の変更によって、購入予定の書籍を遅らせた。
|
| Expenditure Plan for Carryover Budget |
国際会議に論文を投稿するので、その旅費と参加費として利用する。形式検証を加速するため、プロジェクトメンバーの開発会議を増やす。
|
