| 研究課題/領域番号 |
22K11902
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| 研究分担者 |
才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 上級主任研究員 (40415641)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2024年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2023年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 型推論 / 型健全性 / 操作的意味論 / プログラムの証明 / 等式理論 / 型システム / コンパイラー / 依存型 / 形式的証明 |
|---|
| 研究開始時の研究の概要 |
正しく型付けされたプログラムが実行時にエラーを起さないという型健全性はプログラミング言語の重要な性質であり，その恩恵を受けるために型検査も健全でなければならない．しかし，それを形式的に証明することが煩雑な上に，次々に追加される機能への対応が困難である．
この研究では，型健全性や型検査の健全性をプログラミング言語に対する直接的な証明ではなく，既に論理的健全性が確立されている論理体系への翻訳によって得ようとする．
機能を追加するときに翻訳を拡張すれば十分で，翻訳先の定理証明支援系における自動的な型検査が証明になる．OCamlからCoqへの埋め込みを具体例としてこの方法を実現する．
|
| 研究実績の概要 |
本年度は主にCoqに翻訳されたプログラムの証明方法について研究を行った．証明にはモナド等式理論に基いたMonaeというCoqのプログラム証明ライブラリを使っている．具体的にはプログラミング言語の様々な機能を圏論的なモナドとして表現し，その等式理論によってプログラムを証明する．昨年度は既にCoqgen (我々が開発したOCamlからCoqへのコンパイラとライブラリ) で実装された参照型を扱うモナドを直接にMonaeに埋め込むことで，MonaeによるCoqgenで翻訳されたプログラムの証明を実験的に行った．しかし，翻訳の完全性のためにCoqgenの実装はCoqの論理と矛盾する定義を可能にしており，昨年の翻訳方法ではMonaeの無矛盾性を保証することができなかった．本年度は問題を検証した上で実装を整理し，Coqの制限を解除しない，無矛盾な実装を用意した．また，OCamlから翻訳されたプログラム例を増やし，プログラムの証明に必要な公理(等式)を再構成した．参照型(ポインタ)を含むプログラムについて，通常は分離論理でしか証明できないと認識されているようなプログラムも扱えることを確認した．その結果をCoq Workshop 2023 (ビャウィストク開催) ， TPP 2023 (東京工業大学開催) および APLAS NIER 2023 (台北開催) で発表し，論文「A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory」の一部としてまとめた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本方法がプログラムの証明にも応用できることを確認した．また，記述できるプログラムを制限することで，Coqの無矛盾性に触らない実装法も確立した．
|
| 今後の研究の推進方策 |
今後は翻訳できるプログラムを増やし，OCamlの代替コンパイラとしての地位を高める必要がある．
また，完全な実装法について，Coqの健全性と評価戦略の関連を調べていきたい．
|
