Koji Nakazawa

Publication Activity (10 Years)

Years Active: 2003-2023
Publications (10 Years): 9

Top Topics

Natural Deduction

Classical Logic

Top Venues

Math. Struct. Comput. Sci.

Publications

Hiromasa Hori, Koji Nakazawa, Makoto Tatsuta
Cut elimination for propositional cyclic proof systems with fixed-point operators. CoRR (2023)
Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa
Z property for the shuffling calculus. Math. Struct. Comput. Sci. 32 (7) (2022)
Yuki Honda, Koji Nakazawa, Ken-etsu Fujita
Confluence Proofs of Lambda-Mu-Calculi by Z Theorem. Stud Logica 109 (5) (2021)
Kenji Saotome, Koji Nakazawa, Daisuke Kimura
Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions. FSCD (2021)
Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa
Function Pointer Eliminator for C Programs. APLAS (2021)
Kenji Saotome, Koji Nakazawa, Daisuke Kimura
Restriction on Cut in Cyclic Proof System for Symbolic Heaps. FLOPS (2020)
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. APLAS (2019)
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
Completeness of Cyclic Proofs for Symbolic Heaps. CoRR (2018)
Koji Nakazawa, Ken-etsu Fujita
Compositional Z: Confluence Proofs for Permutative Conversion. Stud Logica 104 (6) (2016)
Koji Nakazawa, Hiroto Naya
Strong Reduction of Combinatory Calculus with Streams. Stud Logica 103 (2) (2015)
Koji Nakazawa, Tomoharu Nagai
Reduction System for Extensional Lambda-mu Calculus. RTA-TLCA (2014)
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
Confluence for classical logic through the distinction between values and computations. CL&C (2014)
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
Monadic translation of classical sequent calculus. Math. Struct. Comput. Sci. 23 (6) (2013)
Koji Nakazawa, Shin-ya Katsumata
Extensional Models of Untyped Lambda-mu Calculus CL&C (2012)
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
Type checking and typability in domain-free lambda calculi. Theor. Comput. Sci. 412 (44) (2011)
Koji Nakazawa, Makoto Tatsuta
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems. Chic. J. Theor. Comput. Sci. 2010 (2010)
Yuki Kato, Koji Nakazawa
Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types. WFLP (2009)
Koji Nakazawa, Makoto Tatsuta
Type Checking and Inference for Polymorphic and Existential Types. CATS (2009)
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. CSL (2008)
Koji Nakazawa, Makoto Tatsuta
Strong normalization of classical natural deduction with disjunctions. Ann. Pure Appl. Log. 153 (1-3) (2008)
Koji Nakazawa
An Isomorphism Between Cut-Elimination Procedure and Proof Reduction. TLCA (2007)
Satoshi Ikeda, Koji Nakazawa
Strong normalization proofs by CPS-translations. Inf. Process. Lett. 99 (4) (2006)
Koji Nakazawa
Confluency and strong normalizability of call-by-value lambda-µ-calculus. Theor. Comput. Sci. 290 (1) (2003)
Koji Nakazawa, Makoto Tatsuta
Strong normalization proof with CPS-translation for second order classical natural deduction. J. Symb. Log. 68 (3) (2003)
Koji Nakazawa, Makoto Tatsuta
Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction". J. Symb. Log. 68 (4) (2003)