Formal Foundations for Verification of Physical and Probabilistic Systems

本プロジェクトの目的は、外界の物理的対象と直接対話し動作するプログラムの品質評価のため、定理証明支援系上の検証基盤の設計に必要な検証技術の研究を行うことである。令和４年度、数学と確率的プログラミング言語に集中した。数学の形式化に関して、MathComp-Analysisによる積分論の形式化を進展させ、新たな概念と定理（ラドン＝ニコディムの定理やカーネルなど）で拡張した。その積分論の形式化を用いて、連続確率論の包括的な形式化を開始した。具体的に、非可算濃度の確率論と離散型確率変数を考慮し、基本的な概念（期待値、分散など）の形式化ができた（コペンハーゲンIT大学と共同研究）。そのため、Infotheoという情報理論の形式化による有限確率形式化の一般化を行ってきた。確率的プログラミング言語に関して、一階プログラミング言語の形式化に成功した。具体的に、カーネルを用いた意味論を形式化し、その形式化を等式推論によるプログラム検証に応用した。また、確率プログラムの記述のため、形式構文の設計を行った。また、具体圏の形式化を含む拡張として抽象圏の形式化を試み、型理論的宇宙の制約解決に関する問題を回避するため非可述的データ型を用いた最初の版を作成した（コペンハーゲンIT大学でこの結果について発表と議論）。また、確率論の定式化の一つの応用として確率的プログラムの差分プライバシーの検証のための論理の定式化がある。令和４年度はその一つとして差分プライバシーに適したモナドの持ち上げの一般論をCoqで形式化した。等式推論技術に関して、Monaeというプログラム検証基盤を非決定性と詳細化で拡張した。連続確率を扱う等式推論の拡張を開始した。また、量子プログラミングに関する形式化実験を行ってきた。

本プロジェクトの目的は、外界の物理的対象と直接対話し動作するプログラムの品質評価のため、定理証明支援系上の検証基盤の設計に必要な検証技術の研究を行うことである。令和４年度、数学と確率的プログラミング言語に集中した。数学の形式化に関して、MathComp-Analysisによる積分論の形式化を進展させ、新たな概念と定理（ラドン＝ニコディムの定理やカーネルなど）で拡張した。その積分論の形式化を用いて、連続確率論の包括的な形式化を開始した。具体的に、非可算濃度の確率論と離散型確率変数を考慮し、基本的な概念（期待値、分散など）の形式化ができた（コペンハーゲンIT大学と共同研究）。そのため、Infotheoという情報理論の形式化による有限確率形式化の一般化を行ってきた。確率的プログラミング言語に関して、一階プログラミング言語の形式化に成功した。具体的に、カーネルを用いた意味論を形式化し、その形式化を等式推論によるプログラム検証に応用した。また、確率プログラムの記述のため、形式構文の設計を行った。また、具体圏の形式化を含む拡張として抽象圏の形式化を試み、型理論的宇宙の制約解決に関する問題を回避するため非可述的データ型を用いた最初の版を作成した（コペンハーゲンIT大学でこの結果について発表と議論）。また、確率論の定式化の一つの応用として確率的プログラムの差分プライバシーの検証のための論理の定式化がある。令和４年度はその一つとして差分プライバシーに適したモナドの持ち上げの一般論をCoqで形式化した。等式推論技術に関して、Monaeというプログラム検証基盤を非決定性と詳細化で拡張した。連続確率を扱う等式推論の拡張を開始した。また、量子プログラミングに関する形式化実験を行ってきた。