Koji Nakazawa

31 papers B 5Misc 1Journal 19Unranked 6
YearRankTypeTitle / Venue / Authors
2026 J jnl
Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions.
Arch. Math. Log.
Kenji Saotome, Koji Nakazawa, Daisuke Kimura, Ayumu Kawasaki
2025 J jnl
Admissibility of Substitution Rule in Cyclic-Proof Systems.
CoRR
Kenji Saotome, Koji Nakazawa
2025 J jnl
Incorrectness Separation Logic with Arrays and Pointer Arithmetic.
CoRR
Yeonseok Lee, Koji Nakazawa
2025 J jnl
Incorrectness Separation Logic with Arrays and Pointer Arithmetic.
J. Inf. Process.
Yeonseok Lee, Koji Nakazawa
2025 J jnl
Relative Completeness of Incorrectness Separation Logic.
CoRR
Yeonseok Lee, Koji Nakazawa
2024 B conf
Relative Completeness of Incorrectness Separation Logic.
APLAS
Yeonseok Lee, Koji Nakazawa
2024 J jnl
Restriction on cut rule in cyclic-proof system for symbolic heaps.
Theor. Comput. Sci.
Kenji Saotome, Koji Nakazawa, Daisuke Kimura
2022 J jnl
Z property for the shuffling calculus.
Math. Struct. Comput. Sci.
Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa
2021 J jnl
Confluence Proofs of Lambda-Mu-Calculi by Z Theorem.
Stud Logica
Yuki Honda, Koji Nakazawa, Ken-etsu Fujita
2021 B conf
Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions.
FSCD
Kenji Saotome, Koji Nakazawa, Daisuke Kimura
2021 B conf
Function Pointer Eliminator for C Programs.
APLAS
Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa
2020 Misc conf
Restriction on Cut in Cyclic Proof System for Symbolic Heaps.
FLOPS
Kenji Saotome, Koji Nakazawa, Daisuke Kimura
2019 B conf
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions.
APLAS
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
2018 J jnl
Completeness of Cyclic Proofs for Symbolic Heaps.
CoRR
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
2016 J jnl
Compositional Z: Confluence Proofs for Permutative Conversion.
Stud Logica
Koji Nakazawa, Ken-etsu Fujita
2015 J jnl
Strong Reduction of Combinatory Calculus with Streams.
Stud Logica
Koji Nakazawa, Hiroto Naya
2014 — conf
Confluence for classical logic through the distinction between values and computations.
CL&C
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
2014 — conf
Reduction System for Extensional Lambda-mu Calculus.
RTA-TLCA
Koji Nakazawa, Tomoharu Nagai
2013 J jnl
Monadic translation of classical sequent calculus.
Math. Struct. Comput. Sci.
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
2012 — conf
Extensional Models of Untyped Lambda-mu Calculus
CL&C
Koji Nakazawa, Shin-ya Katsumata
2011 J jnl
Type checking and typability in domain-free lambda calculi.
Theor. Comput. Sci.
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
2010 J jnl
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems.
Chic. J. Theor. Comput. Sci.
Koji Nakazawa, Makoto Tatsuta
2009 — conf
Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types.
WFLP
Yuki Kato, Koji Nakazawa
2009 — conf
Type Checking and Inference for Polymorphic and Existential Types.
CATS
Koji Nakazawa, Makoto Tatsuta
2008 J jnl
Strong normalization of classical natural deduction with disjunctions.
Ann. Pure Appl. Log.
Koji Nakazawa, Makoto Tatsuta
2008 B conf
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence.
CSL
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano
2007 — conf
An Isomorphism Between Cut-Elimination Procedure and Proof Reduction.
TLCA
Koji Nakazawa
2006 J jnl
Strong normalization proofs by CPS-translations.
Inf. Process. Lett.
Satoshi Ikeda, Koji Nakazawa
2003 J jnl
Confluency and strong normalizability of call-by-value lambda-µ-calculus.
Theor. Comput. Sci.
Koji Nakazawa
2003 J jnl
Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction".
J. Symb. Log.
Koji Nakazawa, Makoto Tatsuta
2003 J jnl
Strong normalization proof with CPS-translation for second order classical natural deduction.
J. Symb. Log.
Koji Nakazawa, Makoto Tatsuta