研究シーズ集

情報・通信 ---------------------------- 2024-19 福田　陽介　助教 数学的理論に基づくプログラム設計 工学部情報工学科 ■研究業績等 【論文】 ・学術論文「A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4(.査読付)」4th International Conference on Formal Structures for Computation and Deduction(FSCD 2019) Article No.20:1-20(共著):2019/06 ・学術論文「A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction(.査読付)」6th International Workshop on Logic, Rationality and Interaction(LORI) 2017 554-569(共著):2017/09 ・学術論文「A Higher-arity Sequent Calculus for Model Linear Logic.」数理解析研究所講究録 2083:76-87(共著):2018/08 【学会発表】 ・An extended SECD machine with a first-class macro mechanism.(情報処理学会プログラミング研究会 第124回プログラミング研究発表会(名古屋)):2019/06/07 ・A Linear-logical Reconstruction of Intuitionistic Modal Logic S4.(FSCD 2019(ドルトムント、ドイツ)):2019/06/28 ・On a computational interpretation of Sequent calculus for modal logic S4.(Second Workshop on Mathematical Logic and its Application(金沢)):2018/03/08 広い範囲では「数理論理学」および「プログラミング言語理論」を専門に研究を行っています。数理論理学は、プログラム設計の文脈において「バグの無いプログラムの作成」や、「安全なプログラミング言語の設計」に重要な役割を果たします。私は、数理論理学の中でも特に証明論や自動定理証明といった分野の技術に基づき、バグやエラーの少ないソフトウェアを作るための理論構築を主な目的として研究を行っています。また、「プログラムの性質(プログラムにバグが無いこと、あるいは計算効率が良い、など)」の正しさを数学的に示す、プログラム検証技術についても興味を持っています。 研究シーズや産官学連携に関連して、私が対応できる主な例は以下の通りです。 1.「正しさが保証されたアルゴリズム設計」 アルゴリズムの正しさ(例:入力と出力の関係が正しく成立する、実行時エラーが起きない、等)を数学的に証明した上で、その数学的な証明そのものから正しいアルゴリズムを自動的に抽出する「証明付きプログラム作成の技術」を用いたアルゴリズム設計。 2.「シフトスケジューリング問題・パズル問題等のプログラムによる解決」 いわゆるシフトスケジューリング問題など、解くべき問題の条件はハッキリしているが通常のプログラミング手法では解決しづらい問題を、数学的な手法(制約プログラミングや最適化理論と呼ばれる分野の枠組み)による解決策の考案。 バグの無いアルゴリズム設計 証明付きプログラム作成 数学的手法による問題解決