法政大学 理工学部 創生科学科

近年、100%証明を信頼するためには、証明をコンピューターを使ってチェックするべきであるという考えが広がりつつあり、静かな革命が起きています。コンピューターがチェックできるような形式で詳細に証明を書き下すことを証明の「形式化」と言います。研究室では、主にプログラム検証（プログラムが正しく動作することの証明）の形式化に取り組んでいます。