プログラム論理研究室

About关于研究室

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

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

Research研究课题

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

※示意图

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

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

※示意图

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

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

※示意图

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

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

Voices学长学姐的评价

评价基于在读（或曾在读）学生的个人经历，不代表研究室官方观点。评价的有无或数量不代表对研究室的评价。

对于接受采访的学生，无论内容如何，我们可能会赠送谢礼（价值1,000日元的礼品）。