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 ]
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Restriction on cut in cyclic proof system for symbolic heaps. In The 15th International Symposium on Functional and Logic Programming (FLOPS 2020), Akita, Japan (online), volume 12073 of Lecture Notes in Computer Science (LNCS), pages 88--105, September 2020. [ 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, Ken-etsu Fujita, and Yuta Imagawa. Z for call-by-value. In 6th International Workshop on Cofluence (IWC 2017), Oxford, UK, pages 57--61, September 2017. [ .pdf ]
Koji Nakazawa and Ken-etsu Fujita. Compositional Z: Confluence proofs for permutative conversion. Studia Logica, 104:1205--1224, 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. [ 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. [ 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 ]
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. [ https ]
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, and Keiji Kita. Counterexample generation for symbolic-heap entailment checking. In 2019 SJTU-JAIST-NU Follow-Up Workshop on Formal Methods, Hokkaido, June 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 ]
Koji Nakazawa, Makoto Tatsuta, and Daisuke Kimura. Satisfiability checking for symbolic heaps with cell predicates. SJTU-JAIST-NU Follow-Up Workshop of Formal Methods, Kirishima, June 2018.
Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa. Z for call-by-value. 10th NSFC-JSPS Joint Workshop on Formal Methods, Xian, China, November 2017.
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.
Makoto Tatsuta, Daisuke Kimrua, and Koji Nakazawa. Cyclic-proof-based decision procedure for symbolic heaps and inductive definitions. 2nd Workshop on New and Emerging Results in Programming Languages and Systems, Halong Bay, Vietnam, November 2016.
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. 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. 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. 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. 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.