2015年11月17日中澤 巧爾 准教授（情報システム学専攻）2015/10/1着任

京都大学で学位取得後、同情報学研究科助手、助教を経て、2015年10月より名古屋大学に着任いたしました。

計算と論理の関係について興味を持ち、この関係を通して、プログラムの意味の解析や、論理体系の計算論的な側面を明らかにすることを目標として研究しています。さらに、理論的な成果をプログラムの検証技術に結びつけることを目指しています。

そもそも計算の概念は、今から100年ほど前から始まる数学や論理の土台を整備するの流れの中で明確にされたものであり、論理学とは切っても切れない関係にあります。現代数学を大きく変えたゲーデルの不完全性定理は、計算概念の明確化とその限界を示した定理だとも言えるでしょう。その後、コンピュータの登場によって計算概念はプログラムという形でより具体的な対象となりましたが、このプログラムも、それが満たすべき「仕様」という命題が充足可能であることを示す「証明」であると見做すことができます。この関係性をより厳密に推し進めた結果がカリー・ハワード同型と呼ばれる対応関係です。この関係のもとでは、プログラミング言語（の型システム）と論理における証明体系は全く同じものであると考えることができます。
また、ソフトウェア開発の側からの動機においても、プログラムの厳密な検証を行なうためには、プログラムの意味を正確に捉える必要がありますが、これを実現するために多くの形式論理学における手法が用いられています。例えば、プログラムの振舞いを数学的に定義したり（操作的意味論）、プログラムが満たす性質を確かめたり（型システムやホーア論理）するために、論理学における「証明」の概念が重要な役割を果たしています。
このように、計算機科学と論理学は両者の間の美しい関係を通して相互に影響を及ぼしながら発展してきました。

とくに私が興味を持って研究しているテーマは、カリー・ハワード同型の拡張とその応用です。
もともとこの同型対応は、直観主義論理（我々が通常考える古典論理を制限したもの）と、ごく単純な機構のみをもつプログラミング言語（単純型付ラムダ計算）の間に見出されたものでしたが、1990年代ごろから、その古典論理への拡張が盛んに議論されるようになりました。大きな知見として、古典論理の公理である「二重否定除去」がプログラムにおける実行フローを制御する演算子の型に対応することや、古典論理の顕著な特徴であるド・モルガン双対性がプログラムの評価戦略（CやMLなどに見られる先行評価と、Haskellに見られる遅延評価）の間の双対性に対応することなどが発見されています。このような古典論理に対応する計算体系がもつ意味や、いくつかの基本的な性質を明らかにしたことが、私のこれまでの研究の成果の一つです。
古典論理は、その証明可能性においては、よく知られた真偽値の意味論（ブール代数）で比較的簡単に捉えることができますが、古典論理における証明がもつ計算論的な側面はまだまだ不明な部分が大きく、これを明らかにするのが研究の一つの大きな目標です。また、同型対応の拡張により、より高度な機構をもったプログラミング言語の解析を実現したり、その型システムの正当性に対する裏付けを与え、ソフトウェア検証の技術に応用することも、また一つの大きな研究目標です。