程序逻辑研究室

About关于研究室

致力于通过基于逻辑的理论来保证软件的正确性。

程序逻辑研究室以保证软件的正确性为大目标，研究基于逻辑的软件基础理论。
该研究室将这些理论应用于软件的验证、合成、变换等研究。
研究的支柱包括：基于λ演算和类型论的程序语言理论、程序变换，以及通过模型检测和定理证明进行的验证。
该研究室由亀山幸義教授主持，所属学生来自本科的信息科学类和研究生院的信息理工学位项目。

Research研究课题

该研究室以保证软件的正确性为大目标，构建基于逻辑的软件基础理论，并将这些理论应用于软件的验证、合成、变换等研究。

※示意图

程序的逻辑与类型理论↗

研究许多先进程序语言核心中的函数概念和类型系统的性质。阐明程序（计算）的语义，并进行验证、合成、正确的变换等。

※示意图

程序变换与部分求值↗

利用部分求值的方法，研究在保持正确性的前提下将程序变换为高效程序的技术。例如，定理证明系统的部分求值，以及执行部分求值的系统的构建。

※示意图

通过模型检测和定理证明进行验证↗

为了证明软件是正确的，研究定理证明和模型检测这两种有效的方法。例如，通过模型检测对并行算法进行验证，以及实时模型检测。

Voices学长学姐的评价

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

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