プログラム論理研究室

About研究室について

ソフトウェアの正しさの保証を、論理に基づく理論でめざす。

プログラム論理研究室は、ソフトウェアの正しさを保証することを大きな目標に、論理に基づくソフトウェアの基礎理論を研究しています。
その理論を、ソフトウェアの検証、合成、変換などに応用する研究を行っています。
研究の柱は、ラムダ計算と型理論に基づくプログラム言語の理論、プログラム変換、モデル検査や定理証明による検証です。
亀山幸義教授が主宰する研究室で、学部は情報科学類、大学院は情報理工学位プログラムの学生が所属しています。

Research研究テーマ

ソフトウェアの正しさの保証を大目標に、論理に基づくソフトウェアの基礎理論を築いています。その理論を、ソフトウェアの検証、合成、変換などに応用する研究を行っています。

※イメージ画像

プログラムの論理と型の理論↗

多くの先進的なプログラム言語の中核にある、関数の概念と型システムの性質を研究しています。プログラム（計算）の意味を明確にし、検証、合成、正しい変換などを行います。

※イメージ画像

プログラム変換と部分計算↗

正しさを保ったまま、効率的なプログラムへ変換する技法を、部分計算の手法で研究しています。例として、定理証明システムの部分計算や、部分計算を行うシステムの構築があります。

※イメージ画像

モデル検査と定理証明による検証↗

ソフトウェアが正しいことを証明するため、有力な方法である定理証明とモデル検査を研究しています。例として、並列アルゴリズムのモデル検査による検証や、実時間モデル検査があります。

Voices先輩の声

評価・クチコミは、在籍している（していた）学生個人の経験に基づくもので、研究室の公式見解ではありません。クチコミの有無や件数は、研究室の評価を表すものではありません。

インタビューに協力いただいた学生に、内容にかかわらず謝礼（1,000円分のギフト）をお渡しすることがあります。