研究プロジェクト
物理的・確率的システムの検証を支える形式的基盤の構築

お知らせ

タグ : 全て

Date order : New / Old

現在お知らせはございません

PI	Affeldt Reynald
期間	2022-2025
内容	今日, コンピュータプログラムは, デジタル情報の操作やそのネットワークに加えて, 外界との相互作用を行うため, プログラムの検証には, 形式論理と離散数学だけでなく, 実解析や確率論や幾何学などの数学が必要となり, プログラムの様々な副作用の厳密な検証が困難になっている. その複雑さを抑えるためには, プログラムの意味論の基礎的な研究と, 高度な数学に一貫性のある形式表現を与える統合的な研究の双方が必要である. 本研究では, 定理証明支援系Rocq上, 実解析, 連続確率, 剛体幾何を形式化し, モナドと等式推論に基づいて, 形式的基盤の構築とその評価を行う.
関連研究グループ	超分散トラスト研究グループ
外部連携	名古屋大学, 京都産業大学, 東北大学, 九州大学
外部WEBサイト	https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-22H00520/