数学と情報科学にまたがる学際的領域の研究を行っています。数学としては、数理論理学、数学基礎論、情報科学としては、数理情報科学、理論計算機科学に分類されます。特に、構成的数学、数理論理学、計算の理論を中心に研究を行っています。

構成的数学

　Brouwerの直観主義数学に始まり、HeytingやKolmogorovにより形式化された直観主義論理を用いた数学（構成的数学）を研究しています。Hilbert空間、Banach空間、超関数論などの関数解析学や、その基礎を与えるneighbourhood space、formal topology、basic pairなどの位相空間論を構成的数学の枠組みで研究しています。また、構成的数学の基礎付けとして、構成的集合論、特にMartin-Löfの型理論で自然に解釈できる可術的な集合論CZFを中心に研究を行っています。さらに、通常の数学（古典的数学）、Brouwerの直観主義数学、Markovの構成的数学など様々な哲学のもとに展開された数学を、統一的な視点から論理的原理や関数の存在公理により分類し、整理し、体系化することを目指して構成的逆数学を提唱し、研究を推進しています。

数理論理学

　構成的数学で用いる直観主義論理の証明論や意味論を研究しています。直観主義論理の証明とプログラム（ラムダ計算の項）の間には、Curry-Howardの対応と呼ばれる自然な対応があり、証明からプログラムを合成できます。そのためのシステム（ミュンヘン大学のMinlogシステムなど）が開発されています。古典論理と直観主義論理の関係を明らかにし、古典論理の証明から直観主義論理の証明を取り出し、プログラム合成を行うための基礎研究を行っています。また、線形論理に代表される、部分構造論理の証明論や意味論の研究も行っています。

計算の理論

　計算可能性理論や計算の複雑さ理論の研究と、それらと構成的数学の関係の研究を行っています。多項式時間計算可能関数などの計算可能関数のfunction algebraによる特徴づけ、計算の複雑さや決定不可能次数と構成的逆数学における論理的原理や関数の存在公理の関係を明らかにする研究を目指しています。また、ラムダ計算と単純型、共通部分型、和集合型などの型理論の研究も行っています。

　理論研究は、各自の問題意識に基づいて、自主的に行うものです。学生各自の自主性を尊重し、研究指導を行っています。本研究室で研究指導を希望する学生はここをご覧ください。

　博士前期（修士）課程学生は、今までに構成的数学、数理論理学、圏論、ラムダ計算、計算の複雑さ理論、アルゴリズム的情報理論、量子計算、オートマトン理論、形式言語理論などのテーマで研究を行っています。また、今までに以下の方々が博士後期（博士）課程を修了しました。

• 青戸等人（現新潟大学大学院・自然科学研究科・教授）、On some characterizations of implicational formulas in intuitionistic logic、1997年
• 上出哲広（現帝京大学・理工学部・准教授）、Substructural logics with restricted versions of structural rules、2000年
• 石井克正、Proof theoretical investigations for Visser’s logic, classical logic and the first-order arithmetic、2002年
• 菊池健太郎（現東北大学・電気通信研究所・助教）、Gentzen style sequent calculi for some subsystems of intuitionistic logic、2002年
• 吉田聡（現公立鳥取環境大学大学院・環境情報学研究科・准教授）、A constructive study of the fundamental theory of distributions、2003年
• 河井達治（現北陸先端科学技術大学院大学・先端科学技術研究科・助教）、Bishop compactness in formal topologies、2015年
• 仁木哲（現ルール大学ボーフム・第一哲学科・博士研究員）、Investigations into intuitionistic and other negations、2021年