Validating the type soundness of a programming language through translation into a logical system
| Project/Area Number |
22K11902
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100)
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2024: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2023: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | 型推論 / 型健全性 / 操作的意味論 / プログラムの証明 / 等式理論 / 型システム / コンパイラー / 依存型 / 形式的証明 |
|---|
| Outline of Research at the Start |
正しく型付けされたプログラムが実行時にエラーを起さないという型健全性はプログラミング言語の重要な性質であり，その恩恵を受けるために型検査も健全でなければならない．しかし，それを形式的に証明することが煩雑な上に，次々に追加される機能への対応が困難である．
この研究では，型健全性や型検査の健全性をプログラミング言語に対する直接的な証明ではなく，既に論理的健全性が確立されている論理体系への翻訳によって得ようとする．
機能を追加するときに翻訳を拡張すれば十分で，翻訳先の定理証明支援系における自動的な型検査が証明になる．OCamlからCoqへの埋め込みを具体例としてこの方法を実現する．
|
| Outline of Annual Research Achievements |
関数型プログラミング言語OCamlの型付中間表現であるTypedtreeを定理証明支援系Coqの内部言語であるGallinaに変換するという基本構想を定め，実装を始めた．なお，Typedtreeに型情報が付随しているもの，型推論によるものであり，独立した整合性の確認が行われていない．対して，Gallinaについて厳格な型の確認が行われており，この変換で信頼性が上がるといえる．
実装において，CoqのライブラリとしてOCamlプログラムの副作用(可変な参照型，例外処理など)を扱うモナドを定義し，OCamlのコンパイラがこのモナドを使うGallinaのコードを生成できるように拡張した．変換したプログラムが実行可能で，動作が変わらないことも確認した．代数的データ，再帰関数やループも扱えるようにし，徐々に機能を増やしている．この方法でGADTも表現可能であることも確認したが，コンパイラでは未実装である．
モナドを定義する際，Coqの型定義の制限を緩和する必要があり，結果的にCoqの論理が無矛盾でなくなることを確認したが，モナドの利用方法を制限した場合についてはまだ検討中である．
さらに，この変換をプログラムの証明にも使えるようにするために，上記のモナドの等式理論を定義し，プログラム証明ライブラリMonaeで使えるようにした．それを使って，参照型を使った関数の正しさの証明も行い，実用性を確認した．
上記についてTYPES 2022(フランスのナント開催)，ML Workshop 2022(リュブリャーナ開催)，JSSST 2022およびPPL 2023(名古屋開催)で報告している．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
実装に関して順調に進んでおり，次々と機能が取り込まれている．
理論に関して，型定義の制限を緩和しながらCoqの健全性が保たれる条件がまだ見付かっていないが，問題が評価戦略と関わっていることが見えてきた．
|
| Strategy for Future Research Activity |
今後は引き続き実装を拡張しながら，理論的な側面を解明していきたい．
特にCoqの健全性について，評価戦略との関連を調べていきたい．
また，この変換方法をプログラムの証明に活用できるように，等式理論をさらに検証する予定である．
|
Report
(1 results)
Research Products
(5 results)
