本研究室は「ソフトウェアの基礎理論」をテーマとして研究を行っています。ソフトウェアはスマホやパソコン、銀行のシステム、車や飛行機の制御などあらゆる電子機器の中で動作しており、我々は日常の手助けだけでなく、人命や経済活動の中枢すらも（きっと正常に動作するであろう）ソフトウェアに委ねながら生活しています。しかし、ソフトウェアの多くは人間の手作業のプログラミングによって作成される以上、常にプログラムの誤り(バグ)がつきものです。バグを未然に防ぐ、もしくは書かれたプログラムに潜むバグを発見する手法の確立は現代社会において非常に重要な研究テーマの1つです。
本研究室では、ソフトウェアの安全性の向上を大目標として、プログラム検証、関数型プログラミング言語理論、および型理論の研究を行っています。

プログラム検証
既に書かれたプログラムが仕様(プログラマの意図)通りであるかを確認することをプログラム検証といいます。C言語などのポインタを用いてメモリ操作を記述できるプログラムにおいて、メモリ操作に関するバグはソフトウェアの不具合の原因であったり、バッファオーバーフローやメモリリークなどセキュリティ上の問題の原因になります。このようなバグがないことを数学的に保証するために、分離論理を用いた検証方法の理論的確立とそれに基づく全自動検証ツールの作成を目的として研究を行っています。

関数型プログラミング言語理論
関数型プログラミング言語は「プログラムとは，入力を受けとり結果を出力する関数を記述することである」という理念から設計されているプログラミング言語です。その最大の利点は、数学との親和性が高いことにあり、再帰を用いた数学的な関数の定義がそのままプログラムになります。関数型プログラミング言語における実際のプログラム作成は、正しさのチェックがしやすい小さな関数をいくつか作、それらを関数合成によって繋げていく手法を取ります。これにより、もし問題があったらプログラムを細かく分割して確認できるため、バグの発見に役立ちます。
関数型言語の多くはラムダ計算と呼ばれる計算モデルを用いて研究、設計されています。当研究室では、特に継続機構や多段階計算の機構をもつラムダ計算について研究しています。

型理論
「型」とは，整数型やブール型などの多くのプログラミング言語で用いられているデータ型の概念を抽象化した数学的概念です。この型についての性質を研究する理論が型理論です。上記の関数型プログラミング言語は、関数がもつ型「関数型」を主軸として設計されており、関数型プログラミング言語の基礎理論であるとも言えます。
型はデータ型として解釈できると同時に、論理式としても解釈することができます。例えば、AからBへの関数型A→Bは論理式「AならばB」とも解釈できる、といった具合です。この翻訳を通すことで、計算としての関数型プログラミング言語と論理における証明システムの間に本質的に同等な対応関係（カリー・ハワード同型対応）を見い出すことができます。この対応関係を通すことで、数理論理学で得た知見をプログラミング言語理論に応用したり、論理体系に内在する計算機構の分析をすることができます。当研究室では、特に古典論理や様相論理に内在する計算機構について研究しています。