研究内容

直観主義論理の研究

数学で行われる「証明」を形式化して研究します。特に、直観主義論理と呼ばれる論理に基づいた証明の形式体系に興味があります。

ラムダ計算の研究

「計算」概念を形式化した体系の一つであるラムダ計算について研究を行っています。また、ラムダ計算と直観主義論理の間にあるCurry-Howard対応と呼ばれる対応関係にも興味があります。