中澤 巧爾 助教

電話 075-753-5968
FAX: 075-753-4954
Email: knak@kuis.kyoto-u.ac.jp

オフィス：工学部10号館1階143号室

平成20年12月現在

• 研究テーマ
  
  • プログラミング言語の基礎理論
  • ラムダ計算と型理論
  • 古典論理に基づく計算体系

• 最近の主要論文・著書
  
  • Koji Nakazawa and Makoto Tatsuta.
    Type checking and inference for polymorphic and existential types.
    In Computing: The Australasian Theory Symposium (CATS 2009), to appear.
  • Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano.
    Undecidability of type-checking in domain-free typed lambda-calculi with existence.
    In Computer Science Logic (CSL 2008), LNCS 5213, pp. 478--492 (2008).
  • Koji Nakazawa and Makoto Tatsuta.
    Strong normalization of classical natural deduction with disjunctions.
    Annals of Pure and Applied Logic. 153:21--37 (2008).
  • Koji Nakazawa.
    An isomorphism between cut-elimination procedure and proof reduction.
    Typed Lambda Calculi and Applications (TLCA2007), LNCS 4583, pp. 336-350 (2007).
  • Satoshi Ikeda, Koji Nakazawa.
    Strong Normalization Proofs by CPS-translations.
    Information Processing Letters, 99(4):163-170 (2006).
  • Koji Nakazawa, Makoto Tatsuta.
    Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction.
    Journal of Symbolic Logic, 68(3):851-859 (2003).
    (Corrigendum to this paper has been published in JSL 68(4):1415-1416 (2003).)

• 研究助成（平成10年度以降）
  
  • 科研費 若手研究(B)，古典論理の構文論的双対性とその計算論的意味，(代表)，H18-H20.
  • 科研費 若手研究(B)，古典論理に基づく非決定的計算体系，(代表), H16-H17.

• 学位
  京都大学博士（理学）

• 所属学会
  ACM, 日本ソフトウェア科学会

教育活動

• 担当授業科目(学部)
  計算機科学実験及演習 3（工学部情報学科計算機科学コース）, 2005-2008.
  計算機科学実験及演習 1（工学部情報学科計算機科学コース）, 2004.
  基礎情報処理演習（全学）, 2003.
  

• 学会活動
  
  • 第9回プログラミングおよびプログラミング言語ワークショップ(PPL2007), 実行委員長 (2007.3)
  • 第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009), プログラム委員 (2009.3)

• 学内委員
  
  • 計算機委員会委員（情報学科計算機科学コース）

• 研究室内のページ
• ソフトウェア基礎論分野
• 知能情報学専攻