情報論理学

情報基礎科学専攻

情報論理学 A13 Logic for Information Science

中野圭介教授（Prof. Keisuke Nakano）
浅田和之助教（Assis. Prof. Kazuyuki Asada）
菊池健太郎助教（Assis. Prof. Kentaro Kikuchi）

研究キーワードプログラミング言語理論、形式言語理論、定理証明

ヒトとコンピュータのギャップを埋める

　本研究室の究極的な目標は、プログラミングにおける人間と計算機の隔たりを埋めることです。人間に合わせた記述では実行効率が下がって計算機に負担がかかり、計算機に合わせた記述では開発効率が下がって人間に負担がかかります。そこで、人間に合わせた記述から計算機に合わせた記述を導く「プログラム変換」や、計算機に合わせた記述が人間の意図に沿っているかを保証する「プログラム検証」に取り組んでいます。

　本研究室では、プログラムや計算を抽象化した構造を扱うことのできる「形式木言語理論」を中心に研究を進めています。具体的には、木オートマトンや木トランスデューサなどの理論に基づき、効率的なプログラムを導出したり、プログラマが望む計算の性質を保証したりする枠組みを開発しています。理論の正当性を確認するために定理証明支援系とよばれるツールを用いた研究も進めています。

　このほか、「プログラミング言語意味論」の研究も行っています。こちらの手法では、プログラムの意味をすべて保持した抽象化を行い、それを数学的に分析することにより、対象となる言語の本質を明らかにします。具体的には、表示的意味論・操作的意味論・公理的意味論・圏論的意味論などを、言語の理論的設計やプログラム検証に応用します。

形式木言語理論に裏付けられたプログラム変換による効果を示す実験結果（既存の実装と比較して時間効率も空間効率も改善が見られる）
ジャグリングのパターンの妥当性の余帰納的形式化および定理証明支援システムCoqによるその正当性の証明