2023 Fiscal Year Research-status Report

Validating the type soundness of a programming language through translation into a logical system

Research Project

Project/Area Number	22K11902
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
Keywords	型推論 / 型健全性 / 操作的意味論 / プログラムの証明 / 等式理論
Outline of Annual Research Achievements	本年度は主に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」の一部としてまとめた．
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	今後は翻訳できるプログラムを増やし，OCamlの代替コンパイラとしての地位を高める必要がある．また，完全な実装法について，Coqの健全性と評価戦略の関連を調べていきたい．
Causes of Carryover	本年度は海外渡航の一部を異る財源から支出することができたので，余剰金ができた．来年度は成果発表のためにいくつかの渡航を予定しており，研究費をほぼ使い切る予定である．