教員紹介：中澤 巧爾（なかざわ こうじ）

准教授
http://www.sqlab.i.is.nagoya-u.ac.jp/~nakazawa/

研究内容

「計算」と「論理」という一見独立しているように見える二つの概念の間には実は密接な関係があり、この関係は古くから計算機科学と数理論理学の両面から研究されています。この関係を通して、プログラムの意味の解析や、論理、とくに「証明」がもつ計算論的な構造を明らかにすることを目標として研究しています。とくに、古典論理がもつド・モルガン双対性が、プログラミング言語における異なる評価順序の間の関係に対応することなど、理論的に興味深い結果が得られています。さらにこれらの理論的な成果を基礎として、型システムやプログラム論理（ホーア論理・分離論理）を用いた静的検証などのソフトウェア検証技術に結びつけることを目指しています。