Kenji Saotome and Koji Nakazawa. Cyclic-proof systems for symbolic heaps require cut formulas outside initial signatures. Journal of Information Processing, to appear.
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Restriction on cut rule in cyclic-proof system for symbolic heaps. Theoretical Computer Science, 1019, December 2024. (Extended version of the precedent conference paper in FLOPS 2020.). [ DOI ]
Yeonseok Lee and Koji nakazawa. Relative completeness of incorrectness separation logic. In The 22nd Asian Symposium on Programming Languages and Systems (APLAS 2024), Kyoto, Japan, volume 15194 of Lecture Notes in Computer Science (LNCS), 2024. [ DOI ]
Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, Mirai Ikebuchi, and Koji Nakazawa. Bi-abduction in separation logic with arrays and lists for program analysis. Computer Software, 41:50--67, 2024. (Revised version of the proceeding in PPL2022.). [ DOI ]
Yeonseok Lee and Koji Nakazawa. Decidable entailment checking for concurrent separation logic with fractional permissions. Computer Software, 40, 2023. (Revised version of the proceeding in the 39th JSSST Annual Conference.). [ DOI ]
Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa. Z property for shuffling calculus. Mathematical Structures in Computer Science, 23:1015--1027, August 2022. (Revised version of the precedent workshop paper in IWC2017.). [ DOI ]
Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, and Koji Nakazawa. Function pointer eliminator for C programs (tool paper). In 19th Asian Symposium on Programming Languages and Systems (APLAS), Chicago, US (online), volume 13008 of Lecture Notes in Computer Science (LNCS), pages 23--37, October 2021. [ DOI ]
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Failure of cut-elimination in cyclic proofs of bunched logic with inductive propositions. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Buenos Aires, Argentina (online), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1--11:14, July 2021. [ DOI ]
Yuki Honda, Koji Nakazawa, and Ken-etsu Fujita. Confluence proofs of lambda-mu-calculi by Z theorem. Studia Logica, 109:917--936, 2021. [ DOI ]
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura. Spatial factorization in cyclic-proof system for separation logic. Computer Software, 37:125--144, 2020. (Revised version of the precedent workshop paper in PPL2019.) (JSSST Best Research Paper Award). [ DOI ]
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno. Failure of cut-elimination in cyclic proofs of separation logic. Computer Software, 37:39--52, 2020. (Revised version of the precedent workshop paper in PPL2019.). [ DOI ]
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In The 17th Asian Symposium on Programming Languages and Systems (APLAS 2019), Bali, Indonesia, volume 11893 of Lecture Notes in Computer Science (LNCS), pages 367--387, December 2019. [ DOI ]
Kosuke Fukui and Koji Nakazawa. Complete axiom system of cluster algebra. In 7th International Workshop on Cofluence (IWC 2018), Oxford, UK, July 2018. [ .pdf ]
Koji Nakazawa and Ken-etsu Fujita. Compositional Z: Confluence proofs for permutative conversion, December 2016. [ DOI ]
Koji Nakazawa and Hiroto Naya. Strong reduction of combinatory logic with streams. Studia Logica, 103:375--387, April 2015. [ DOI ]
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 (LNCS), pages 340--363, July 2014. [ DOI ]
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 (EPTCS), pages 63--77, July 2014. [ DOI ]
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 ]
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 (EPTCS), pages 35--47, October 2012. [ DOI ]
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 ]
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.). [ .html ]
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 (LNCS), pages 96--110. Springer, April 2010. [ DOI ]
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 (LNCS), pages 478--492. Springer, September 2008. [ DOI ]
Koji Nakazawa and Makoto Tatsuta. Strong normalization of classical natural deduction with disjunctions. Annals of Pure and Applied Logic, 153:21--37, April 2008. (Revised version of the proceeding in PPL2006.). [ DOI ]
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 (LNCS), pages 336--350. Springer, 2007. [ DOI ]
Satoshi Ikeda and Koji Nakazawa. Strong normalization proofs by CPS-translations. Information Processing Letters, 99(4):163--170, August 2006. (Revised version of the proceeding in PPL2005.). [ DOI ]
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 ]
Koji Nakazawa. Confluency and strong normalizability of call-by-value λμ-calculus. Theoretical Computer Science, 290:429--463, January 2003. [ DOI ]
Yeonseok Lee and Koji Nakazawa. Incorrectness separation logic with arrays and pointer arithmetic. arXiv.org, March 2025. [ DOI ]
Daisuke Kimura, Koji Nakazawa, and Kenji Saotome. Cut-elimination for cyclic proof systems with inductively defined propositions. In Theory and Applications of Proof and Computation, volume 2228 of RIMS Kokyuroku, pages 59--72, August 2022.
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps. arXiv.org, April 2018. [ DOI ]
Kenji Saotome and Koji Nakazawa. Cyclic-proof systems for symbolic heaps require cut formulas outside initial signatures. In The 61st TRS meeting, Kaga, Japan, March 2025.
Yeonseok Lee and Koji Nakazawa. Incorrectness separation logic with arrays and pointer arithmetic. In The 61st TRS meeting, Kaga, Japan, March 2025.
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions. In The 4th Workshop on Mathamatical Logic and Its Applications, online, March 2021.
Koji Nakazawa, Kosuke Fukui, and Saori Ishii. Proof normalization for classical truth-table natural deduction. In The 2019 Joint Workshop on Formal Methods, Shanghai, China, December 2019.
Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome. On cut elimination in cyclic-proof systems. In The 51st TRS meeting, Sounkyo, Japan, September 2019.
Yuuki Honda, Koji Nakazawa, and Ken-etsu Fujita. Confluence proof of lambda-mu-calculus by Z theorem. In The 51st TRS meeting, Sounkyo, Japan, September 2019.
Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome. On cut elimination in cyclic-proof systems. In The 3rd Workshop on Mathamatical Logic and Its Applications, Nancy, France, March 2019.
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with cone inductive definitions. In The 3rd Workshop on Mathamatical Logic and Its Applications, Nancy, France, March 2019.
Daisuke Kimura, Makoto Tatsuta, and Koji Nakazawa. Entailment checking procedure for symbolic heap using complete cyclic proof system. In The 3rd Workshop on Mathamatical Logic and Its Applications, Nancy, France, March 2019.
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome. On cut elimination in cyclic-proof system for separation logic. The 12th Joint Workshop on Formal Methods, Shanghai, China, December 2018.
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno. On cut elimination in cyclic-proof system for separation logic. 16th Asian Symposium on Programming Languages and Systems (APLAS 2018), Poster, Wellington, New Zealand, December 2018. [ .pdf ]
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno. On cut elimination in cyclic-proof system for separation logic. 4th Workshop on New Ideas and Emerging Results (NIER 2018), Wellington, New Zealand, December 2018.
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura. Cyclic theorem prover for separation logic by magic wand. In 1st Workshop on Automated Deduction for Separation Logics (ADSL 2018), Oxford, UK, July 2018. [ .pdf ]
Makoto Tatsuta, Daisuke Kimura, and Koji Nakazawa. Complete cyclic-proof system for separation logic with general inductive predicates. Analysis and Verification of Pointer Programs, No. 100 of NII Shonan Meeting, Shonan, October 2017.
Makoto Tatsuta, Daisuke Kimrua, and Koji Nakazawa. Cyclic-proof-based decision procedure for symbolic heaps and inductive definitions. First NII Programming and Logic Workshop, NII, March 2017.
Koji Nakazawa. Characterizing trees for lambda-mu terms (extended abstract). In 8th International Workshop on Higher-Order Rewriting (HOR 2016), Porto, Portugal, June 2016. [ .pdf ]
Miyamoto, Y., Suenaga, K., and Nakazawa, K. A denotational semantics of a probabilistic stream-processing language. In Workshop on probabilistic programming semantics (PPS 2016), Poster, Florida, US, January 2016.
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. 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.