研究者総覧「情報知」
情報システム学専攻
- 氏 名
- 中澤 巧爾 (なかざわ こうじ)
- 講座等
- ソフトウェア論講座
- 職 名
- 准教授
- 学 位
- 博士（理学）
- 研究分野
- プログラミング言語の理論 / 型理論 / 数理論理学
研究内容
プログラミング言語と論理の対応関係に基づくプログラムの解析と検証
研究背景：プログラムの正しさを厳密に調べるためには、プログラムがどのように動作するか、どのように振る舞うか、といった「プログラムの意味」を正確に理解しなければいけません。プログラミング言語理論の分野では、この「プログラムの意味」を数学的に定義するために、様々な数学的な道具を利用しますが、これらの多くは数学基礎論や数理論理学の分野で、数学を形式的に扱うために導入された概念が基礎となっています。例えば、プログラムの動作の構文論的な定義（操作的意味論）や、プログラムが満たす性質の検証（型システムやホーア論理）のために、論理学における「証明」の概念が重要な役割を果たしています。さらに、プログラムそのものがその仕様の実現可能性を示す一種の「証明」である、という見方から、プログラミング言語と証明体系の間にはさらに直接的な対応関係（カリー・ハワード同型）が見出されており、この対応を通しても、プログラミング言語の理論と数理論理学（とくに、証明そのものを解析する証明論と呼ばれる分野）は相互に影響を及ぼしあって発展しています。
研究概要：プログラミング言語（の型システム）と論理との間の対応関係を通して、プログラムの厳密な解析や、論理が持つ計算論的側面の解明を目的として研究を行っています。また、その理論的成果をプログラム検証に応用することを目指しています。
主な研究テーマ：
1. 様々な論理に対応する計算概念：従来、直観主義論理と極単純なプログラミング言語の間の対応として知られていたカリー・ハワード同型を拡張し、古典論理や様相論理など、様々な論理体系に対応するプログラミング機構を明らかにしたいと考えています。例えば、古典論理のある公理が、プログラムの実行フローを制御するオペレータの型に対応することや、様相論理が多段階計算に対する型システムに対応することが知られています。とくに古典論理に対応する計算体系の性質を調べ、古典論理がもつ計算論的な側面について研究を進めています。
2. 型によるプログラム検証：プログラミング言語の型システムは「型がつくプログラムは間違った振る舞いをしない」ように設計されます。このため、プログラムが型を持つことを判定することによって、プログラムのある種の正しさを検証することができます。単純な機構のみを持つプログラミング言語に対しては、その型システムの型判定が自動化され、実際のプログラミング言語において型による自動検査が実現されています。しかし、より高度な型を無条件に入れると、原理的に型判定が計算不能になることが知られています。豊富な機構をもつプログラミング言語に対して現実的な時間で自動型検査を行うための研究を行っています。
経歴
- 2002年11月 京都大学大学院理学研究科博士課程修了．博士（理学）
- 2002年12月～2006年3月 京都大学大学院情報学研究科助手
- 2006年4月～2015年9月 同助教
- 2009年9月～12月 トゥールーズ第三大学（ポールサバティエ大学）訪問研究員
- 2015年10月～現在 名古屋大学大学院情報科学研究科准教授
所属学会
- JSSST
- MSJ
- EATCS
主要論文・著書
- Koji Nakazawa and Hiroto Naya. Strong reduction of combinatory logic with streams. Studia Logica, 103:375–387, April 2015.
- Koji Nakazawa and Tomoharu Nagai. Reduction system for extensional lambda-mu calculus. In 25th International Conference on Rewriting Techniques and Applications joint with the 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), volume 8560 of Lecture Notes in Computer Science, pages 340–363, July 2014.
- José Espírito Santo, Ralph Matthes, Koji Nakazawa, and Luís Pinto. Monadic translation of classical sequent calculus.Mathematical Structures in Computer Science, 23:1111–1162, December 2013.
- Koji Nakazawa and Shin-ya Katsumata. Extensional models of untyped lambda-mu calculus. In Herman Geuvers and Ugo de'Liguoro, editors, Proceedings Fourth Workshop on Classical Logic and Computation (CL&C 2012), volume 97 ofElectric Proceedings in Theoretical Computer Science, pages 35–47, October 2012.
- Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano. Type checking and typability in domain-free lambda calculi. Theoretical Computer Science, 412(44):6193–6207, October 2011.
- Koji Nakazawa and Makoto Tatsuta. Strong normalization of classical natural deduction with disjunctions. Annals of Pure and Applied Logic, 153:21–37, April 2008.
- Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications (TLCA2007), volume 4583 of Lecture Notes in Computer Science, pages 336–350. Springer, 2007.
- Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications (TLCA2007), volume 4583 of Lecture Notes in Computer Science, pages 336–350. Springer, 2007.
- Koji Nakazawa and Makoto Tatsuta. Strong normalization proof with CPS-translation for second order classical natural deduction. The Journal of Symbolic Logic, 68(3):851–859, September 2003.
- Koji Nakazawa. Confluency and strong normalizability of call-by-value λμ-calculus. Theoretical Computer Science, 290:429–463, January 2003.
