Syntactic Duality of Classical Logic and Its Computational Aspect

• Project/Area Number: 18700008
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Fundamental theory of informatics
• Research Institution: Kyoto University
• Principal Investigator: NAKAZAWA Koji Kyoto University, 大学院・情報学研究科, 助教 (80362581)
• Project Period (FY): 2006 – 2008
• Project Status: Completed (Fiscal Year 2008)
• Budget Amount: ¥2,510,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥210,000); Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2007: ¥700,000 (Direct Cost: ¥700,000); Fiscal Year 2006: ¥900,000 (Direct Cost: ¥900,000)
• Keywords: 古典論理 / シーケント計算 / カット除去 / 自然演繹 / カリーハワード同型 / 存在型 / 型検査 / 型推論 / 決定問題 / CPS変換 / 置換簡約 / 一般除去規則 / 自然演出繹 / 証明正規化 / 強正規化性 / 合流性

Research Abstract

本研究では以下の結果を得た。(1) 直観主義シーケント計算のカット除去として、自然演繹の証明正規化と同型であるものを提案した。(2) 存在型を持つ型付きラムダ計算における型検査問題、型推論問題が決定不能であることを証明した。

Research Products

• [Journal Article] Type Checking and Inference for Polymorphic and Existential Types. (2009)
  • Author(s): Koji Nakazawa and Makoto Tatsuta
  • Journal Title: Computing : The Australasian Theory Symposium (CATS2009) (CD-ROM)
  • Peer Reviewed
• [Journal Article] Type Checking and Inference for Polymorphic and Existential Types (2009)
  • Author(s): K. Nakazawa and M. Tatsuta
  • Journal Title: Computing : The Australasian Theory Symposium (CATS'09) (CD-ROM)
  • Peer Reviewed
• [Journal Article] Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. (2008)
  • Author(s): Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
  • Journal Title: Computer Science Logic (CSL' 08), Lecture Notes in Computer Science 5213 Pages: 478-492
  • Peer Reviewed
• [Journal Article] Strong Normalization of Classical Natural Deduction with Disjunctns (2008)
  • Author(s): Koji Nakazawa and Makoto Tatsuta
  • Journal Title: Annals of Pure and Applied Logic 153 Pages: 21-37
  • Peer Reviewed
• [Journal Article] Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence (2008)
  • Author(s): K. Nakazawa, M. Tatsuta, Y. Kameyama, and H. Nakano
  • Journal Title: Computer Science Logic (CSL'09) Pages: 478-492
  • Peer Reviewed
• [Journal Article] Strong normalization of classical natural deduction with disjunctions (2008)
  • Author(s): Koji Nakazawa and Makoto Tatsuta
  • Journal Title: Annals of Pure and Applied Logic 153 Pages: 21-37
  • Peer Reviewed
• [Journal Article] An Isomorphism between Cut-Elimination Procedure and Proof Reduction (2007)
  • Author(s): Koji Nakazawa
  • Journal Title: Typed Lambda Calculi and Applications (TLCA' 07), Lecture Notes in Computer Science 4583 Pages: 336-350
  • Peer Reviewed
• [Journal Article] An Isomorphism Between Cut-Elimination Procedure and Proof Reduction (2007)
  • Author(s): Koji Nakazawa
  • Journal Title: Typed Lambda Calculi and Applications (TLCA2007) Pages: 336-350
  • Peer Reviewed
• [Journal Article] An isomorphism between cut-elimination procedure and proof reduction (2007)
  • Author(s): Koji Nakazawa
  • Journal Title: Typed Lambda Calculi and Applications (TLCA'07) (To appear)
• [Journal Article] Strong Normalization Proofs by CPS-Translations (2006)
  • Author(s): Satoshi Ikeda and Koji Nakazawa
  • Journal Title: Information Processing Letters 99 Pages: 163-170
  • Peer Reviewed
• [Journal Article] Strong normalization proofs by CPS-translations (2006)
  • Author(s): Satoshi Ikeda, Koji Nakazawa
  • Journal Title: Information Processing Letters 99 Pages: 163-170
• [Presentation] 存在型に対する型検査問題と型推論問題の同値性 (2009)
  • Author(s): 加藤祐輝, 中澤巧爾
  • Organizer: 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009), ポスター
• [Presentation] An Isomorphism between Cut-Elimination Procedure and Proof Reduction (2007)
  • Author(s): Koji Nakazawa
  • Organizer: SCORE Summer Workshop on Symbolic Computation and Software Verification
• [Presentation] trong Cut-Elimination and CPS-Translations. (In T. Kutsia and M. Marin, eds.) (2007)
  • Author(s): Koji Nakazawa
  • Organizer: Austria-Japan Workshop on Symbolic Computation and Software Verification, No. 07-09 in RISC-Linz Report Series,