Syntactic Duality of Classical Logic and Its Computational Aspect

2008 Fiscal Year Final Research Report

• 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
• Keywords: 古典論理 / シーケント計算 / カット除去 / 自然演繹 / カリーハワード同型

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] 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] 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] 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
• [Presentation] 存在型に対する型検査問題と型推論問題の同値性 (2009)
  • Author(s): 加藤祐輝, 中澤巧爾
  • Organizer: 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009), ポスター
  • Year and Date: 20090000
• [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
  • Year and Date: 20070000
• [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,
  • Year and Date: 20070000