List of Publications by Koji Nakazawa

[Japanese]

Papers

• 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. (Extended version of the precedent conference paper in CSL2008.). (PDF)

• Yuki Kato and Koji Nakazawa. Type checking and inference are equivalent in lambda calculi with existential types. In Santiago Escobar, editor, 18th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2009), Revised Selected Papers, Brasilia, Brazil, volume 5979 of Lecture Notes in Computer Science, pages 96–110. Springer-Verlag, April 2010. (PDF)

• Koji Nakazawa and Makoto Tatsuta. Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems. Chicago Journal of Theoretical Computer Science, Special Issue: Selected papers from 2009 Computing: The Australasian Theory Symposium (CATS 2009), Article 7, 2010. (Jounal version of the precedent conference paper: Type Checking and Inference for Polymorphic and Existential Types, CATS 2009, Wellington, New Zealand, January, 2009.). (PDF)

• Koji Nakazawa and Makoto Tatsuta. Strong normalization of classical natural deduction with disjunctions. Annals of Pure and Applied Logic, 153:21–37, April 2008. (PDF)

• Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano. Undecidability of type-checking in domain-free typed lambda calculi with existence. In Michael Kaminski and Simone Martini, editors, Computer Science Logic (CSL 2008), Bertinoro, Italy, volume 5213 of Lecture Notes in Computer Science, pages 478–492. Springer-Verlag, September 2008. (PDF)

• 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-Verlag, 2007. (PDF)

• Satoshi Ikeda and Koji Nakazawa. Strong normalization proofs by CPS-translations. Information Processing Letters, 99(4):163–170, August 2006. (PDF)

• Koji Nakazawa. Confluency and strong normalizability of call-by-value λμ-calculus. Theoretical Computer Science, 290:429–463, January 2003. (PDF)

• 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. (PDF) Corrigendum of this article is available in, The Journal of Symbolic Logic, 68(4):1415–1416, December 2003. (PDF).

Talks and Others

• Koji Nakazawa. Continuations and classical logic: using continuations as a tool for classical logic. ACM SIGPLAN Continuation Workshop (CW2011), invited talk, September 2011.

• Koji Nakazawa. Monadic translation of classical sequent calculus. MLG44, Hakone, May 2010. Collaborated work with José Espírito Santo, Ralph Matthes, and Luís Pinto.

• Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. SCORE Summer Workshop on Symbolic Computation and Software Verification, Fuji Susono, August-September 2007.

• Koji Nakazawa. Strong cut-elimination and CPS-translations. In T. Kutsia and M. Marin, editors, Austria-Japan Workshop on Symbolic Computation and Software Verification, Linz, number 07-09 in RISC-Linz Report Series, pages 15–16, July 2007.

• Koji Nakazawa. SN proofs by CPS-translations. Kusatsu Seminar 2006 on Lambda Calculus and Logics, Kusatsu, March 2006.

Notice: The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.