研究課題
基盤研究(C)
(1) 二相再帰は、関数定義の定義本体の中の全ての再帰呼び出しが同じ型をもつように制限した多相再帰である。二相再帰が主型をもち、また、決定可能な型推論をもつことを示した。(2) 双対計算を帰納型と余帰納型により拡張した。非決定可能双対計算を定義し、強正規化可能性を示した。値呼び体系と名前呼び体系を定義し、その合流性と強正規化可能性を証明した。(3) 逐次バックトラック付きゲームを提案し、そのゲーム意味論が、部分古典論理に対して、健全かつ完全な意味論を与えることを示した。
プログラム理論
