研究KEYWORD
計算理論，プログラム理論，数理論理学，計算可能性，計算量
研究分野
情報学基礎理論，数学基礎・応用数学
主要な研究内容
数理論理学の観点から，関数型プログラミング言語と古典論理との同型対応関係，古典論理の証明とプロセス計算との関係，プログラムの型推論や検証などの研究に従事してきました。最近では，特に，プログラムの型検査・型推論問題の決定可能性について研究を行っています。
共同研究に応用できる技術分野 または 共同研究実績
プログラム理論，計算理論，数理論理学の応用として，プログラム検証や形式的技法など．
主要な所属学会
情報処理学会，日本ソフトウェア科学会，人工知能学会，EATCS，日本数学会
近年の論文 または 特許 (3件以内)
- The Church–Rosser theorem and quantitative analysis of witnesses（チャーチ・ロッサーの定理と証拠の定量的評価）, Information and Computation 263: 52–56, (2018)
- The undecidability of type related problems in type-free style System F with finitely stratified polymorphic types（タイプフリースタイルのシステムFにおける型問題の決定不能性について）, Information and Computation 218: 69–87, (2012)
- CPS-translation as adjoint（アジョイントとしてのCPS変換）, Theoretical Computer Science, 411(2): 324–340 (2010)