List of Publications by Koji Nakazawa
[Japanese][dblp]
Last Update:
Tue Aug 11 15:36:27 JST 2015
Papers
- Koji Nakazawa and Hiroto
Naya.
Strong reduction of combinatory logic with streams.
Studia Logica, 103:375–387, April 2015.
(doi:10.1007/s11225-014-9570-3)
- José Espírito Santo,
Ralph Matthes, Koji Nakazawa, and
Luís Pinto.
Confluence for classical logic through the distinction between values and
computation.
In Paulo Oliva, editor, The Fifth International Workshop
on Classical Logic and Computation (CL&C'14), volume 164 of
Electric Proceedings in Theoretical Computer Science, pages
63–77, July 2014.
(doi:10.4204/EPTCS.164.5)
- 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.
(doi:10.1007/978-3-319-08918-8_24)
- 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.
(doi:10.1017/S0960129512000436)
- 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 of Electric Proceedings in Theoretical Computer
Science, pages 35–47, October 2012.
(doi:10.4204/EPTCS.97.3)
- 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.).
(doi:10.1016/j.tcs.2011.06.020)
- 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)
- 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, April 2010.
(doi:10.1007/978-3-642-11999-6_7)
- 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,
September 2008.
(doi:10.1007/978-3-540-87531-4_34)
- Koji Nakazawa and Makoto
Tatsuta.
Strong normalization of classical natural deduction with disjunctions.
Annals of Pure and Applied Logic, 153:21–37, April 2008.
(doi:10.1016/j.apal.2008.01.003)
- 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.
(doi:10.1007/978-3-540-73228-0_24)
- Satoshi Ikeda and Koji
Nakazawa.
Strong normalization proofs by CPS-translations.
Information Processing Letters, 99(4):163–170, August 2006.
(doi:10.1016/j.ipl.2006.03.009)
- 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.
Corrigendum of this article is available in, The Journal of Symbolic
Logic, 68(4):1415–1416, December 2003. (doi:10.2178/jsl/1067620196).
(doi:10.2178/jsl/1058448444)
- Koji
Nakazawa.
Confluency and strong normalizability of call-by-value λμ-calculus.
Theoretical Computer Science, 290:429–463, January 2003.
(doi:10.1016/S0304-3975(01)00380-2)
Talks and Others
- Koji
Nakazawa.
Lambda calculi and confluence from A to Z.
4th International Workshop on Confluence (IWC 2015), Invited Talk, Berlin,
August 2015.
- Koji
Nakazawa.
Confluence for lambda calculi with permutative conversion.
In 42nd TRS meetingˇ¤Harumi, Tokyo, February 2015.
- Koji Nakazawa.
Confluence for lambda calculi with permutative conversion.
In 9th NII Type Theory Workshopˇ¤NII, Tokyo, January 2015.
- Koji
Nakazawa.
Extensional models of typed lambda-mu calculus.
In The Fifth International Workshop on Classical Logic and Computation
(CL&C'14), Vienna, short paper, July 2014.
- Koji
Nakazawa.
Continuations and classical logic: using continuations as a tool for classical
logic.
ACM SIGPLAN Continuation Workshop (CW2011), invited talk, Tokyo, 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.
[HOME]