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

点击翻译按钮获取中文摘要

関数型プログラミング言語OCamlの型付中間表現であるTypedtreeを定理証明支援系Coqの内部言語であるGallinaに変換するという基本構想を定め，実装を始めた．なお，Typedtreeに型情報が付随しているもの，型推論によるものであり，独立した整合性の確認が行われていない．対して，Gallinaについて厳格な型の確認が行われており，この変換で信頼性が上がるといえる．実装において，CoqのライブラリとしてOCamlプログラムの副作用(可変な参照型，例外処理など)を扱うモナドを定義し，OCamlのコンパイラがこのモナドを使うGallinaのコードを生成できるように拡張した．変換したプログラムが実行可能で，動作が変わらないことも確認した．代数的データ，再帰関数やループも扱えるようにし，徐々に機能を増やしている．この方法でGADTも表現可能であることも確認したが，コンパイラでは未実装である．モナドを定義する際，Coqの型定義の制限を緩和する必要があり，結果的にCoqの論理が無矛盾でなくなることを確認したが，モナドの利用方法を制限した場合についてはまだ検討中である．さらに，この変換をプログラムの証明にも使えるようにするために，上記のモナドの等式理論を定義し，プログラム証明ライブラリMonaeで使えるようにした．それを使って，参照型を使った関数の正しさの証明も行い，実用性を確認した．上記についてTYPES 2022(フランスのナント開催)，ML Workshop 2022(リュブリャーナ開催)，JSSST 2022およびPPL 2023(名古屋開催)で報告している．