[ English | Japanese ]

Publications

Journal Articles

LMCS 2025
Nao Hirokawa and Aart Middeldorp.
Hydra Battles and AC Termination.
Journal of Logical Methods in Computer Science 21(29), pp. 29:1–29:22, 2025.
doi: 10.46298/lmcs-21(2:29)2025
LMCS 2025
Johannes Niederhauser, Nao Hirokawa, and Aart Middeldorp.
Left-Linear Completion with AC Axioms.
Journal of Logical Methods in Computer Science 21(2), pp. 10:1–10:44, 2025.
doi: 10.46298/lmcs-21(2:10)2025
LMCS 2024
Kiraku Shintani and Nao Hirokawa.
Compositional Confluence Criteria.
Journal of Logical Methods in Computer Science 20(1), pp. 6:1–6:28, 2024.
doi: 10.46298/lmcs-20(1:6)2024 errata
LMCS 2019
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler.
Abstract Completion, Formalized.
Journal of Logical Methods in Computer Science 15(3), pp. 1:1–1:19, 2019.
doi: 10.23638/LMCS-15(3:19)2019 errata
TPLP 2015
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp.
AC-KBO Revisited.
Theory and Practice of Logic Programming 16(2), pp. 163–188, 2015.
doi: 10.1017/S1471068415000083
JAR 2013
Nao Hirokawa, Aart Middeldorp, and Harald Zankl.
Uncurrying for Termination and Complexity.
Journal of Automated Reasoning 50, pp. 279–315, 2013.
doi: 10.1007/s10817-012-9248-3
JAR 2011
Nao Hirokawa and Aart Middeldorp.
Decreasing Diagrams and Relative Termination.
Journal of Automated Reasoning 47, pp. 481–501, 2011.
doi: 10.1007/s10817-011-9238-x
JAR 2009
Harald Zankl, Nao Hirokawa, and Aart Middeldorp.
KBO Orientability.
Journal of Automated Reasoning 43(2), pp. 173–201, 2009.
doi: 10.1007/s10817-009-9131-z
I&C 2007
Nao Hirokawa and Aart Middeldorp.
Tyrolean Termination Tool: Techniques and Features.
Information and Computation 205, pp. 474–511, 2007.
doi: 10.1016/j.ic.2006.08.010
I&C 2005
Nao Hirokawa and Aart Middeldorp.
Automating the Dependency Pair Method.
Information and Computation 199(1,2), pp. 172–199, 2005.
doi: 10.1016/j.ic.2004.10.004

Conference and Workshop Papers

CADE 2025
Teppei Saito and Nao Hirokawa.
Lexicographic Combination of Reduction Pairs.
Proceedings of the 30th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pp. ??–??, 2025.
FSCD 2024
Teppei Saito and Nao Hirokawa.
Simulating Dependency Pairs by Semantic Labeling.
Proceedings of the 9th International Conference on Formal Structures of Computation and Deduction, Leibniz International Proceedings in Informatics 299, pp. 13:1–13:20, 2024.
doi: 10.4230/LIPIcs.FSCD.2024.13
CPP 2024
Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann.
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs.
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 147–161, 2024.
doi: 10.1145/3636501.3636949
FroCoS 2023
Teppei Saito and Nao Hirokawa.
Weighted Path Orders are Semantic Path Orders.
Proceedings of the 14th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 14279, pp. 63–80, 2023.
doi: 10.1007/978-3-031-43369-6_4 best paper award
CADE 2023
Johannes Niederhauser, Nao Hirokawa, and Aart Middeldorp.
Left-Linear Completion with AC Axioms.
Proceedings of the 29th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 14132, pp. 401–418, 2023.
doi: 10.1007/978-3-031-38499-8_23
FSCD 2023
Nao Hirokawa and Aart Middeldorp.
Hydra Battles and AC Termination.
Proceedings of the 8th International Conference on Formal Structures of Computation and Deduction, Leibniz International Proceedings in Informatics 260, pp. 12:1–12:16, 2023.
doi: 10.4230/LIPIcs.FSCD.2023.12
FSCD 2022
Kiraku Shintani and Nao Hirokawa.
Compositional Confluence Criteria.
Proceedings of the 7th International Conference on Formal Structures of Computation and Deduction, Leibniz International Proceedings in Informatics 228, pp. 28:1–28:19, 2022.
doi: 10.4230/LIPIcs.FSCD.2022.28
FSCD 2021
Nao Hirokawa.
Completion and Reduction Orders.
Proceedings of the 6th International Conference on Formal Structures of Computation and Deduction, Leibniz International Proceedings in Informatics 195, pp. 2:1–2:9.
doi: 10.4230/LIPIcs.FSCD.2021.2 errata slides
CADE 2019
Nao Hirokawa, Julian Nagele, Vincent van Oostrom, and Michio Oyamaguchi.
Confluence by Critical Pair Analysis Revisited.
Proceedings of the 27th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 11716, pp. 319–336, 2019.
doi: 10.1007/978-3-030-29436-6_19 extended version
FSCD 2018
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl.
Confluence Competition 2018.
Proceedings of the 3rd International Conference on Formal Structures of Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 32:1–32:5, 2018.
doi: 10.4230/LIPIcs.FSCD.2018.32
IJCAR 2018
Nao Hirokawa, Julian Nagele, and Aart Middeldorp.
Cops and CoCoWeb: Infrastructure for Confluence Tools.
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 346–353, 2018.
doi: 10.1007/978-3-319-94205-6_23
FSCD 2017
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler.
Infinite Runs in Abstract Completion.
Proceedings of the 2nd International Conference on Formal Structures of Computation and Deduction, Leibniz International Proceedings in Informatics 84, pp. 19:1–19:16, 2017.
doi: 10.4230/LIPIcs.FSCD.2017.19
CADE 2015
Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl.
Confluence Competition 2015.
Proceedings of the 25th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 9195, pp. 101–104, 2015.
doi: 10.1007/978-3-319-21401-6_5
CADE 2015
Kiraku Shintani and Nao Hirokawa.
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems.
Proceedings of the 25th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 9195, pp. 127–136, 2015.
doi: 10.1007/978-3-319-21401-6_8
RTA 2015
Nao Hirokawa, Aart Middeldorp, and Georg Moser.
Leftmost Outermost Revisited.
Proceedings of the 26th International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics 36, pp. 209–222, 2015.
doi: 10.4230/LIPIcs.RTA.2015.209
RTA-TLCA 2014
Nao Hirokawa and Georg Moser.
Automated Complexity Analysis Based on Context-Sensitive Rewriting.
Proceedings of the the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 8560, pp. 257–271, 2014.
doi: 10.1007/978-3-319-08918-8_18
ITP 2014
Nao Hirokawa, Aart Middeldorp, and Christian Sternagel.
A New and Formalized Proof of Abstract Completion.
Proceedings of the 5th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 8558, pp. 292–307, 2014.
doi: 10.1007/978-3-319-08970-6_19
FLOPS 2014
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp.
AC-KBO Revisited.
Proceedings of the 12th International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science 8475, pp. 319–335, 2014.
doi: 10.1007/978-3-319-07151-0_20
LPAR 2012
Dominik Klein and Nao Hirokawa.
Confluence of Non-Left-Linear TRSs via Relative Termination.
Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science 7180, pp. 258–273, 2012.
doi: 10.1007/978-3-642-28717-6_21
RTA 2011
Dominik Klein and Nao Hirokawa.
Maximal Completion.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics 10, pp. 71–80, 2011.
doi: 10.4230/LIPIcs.RTA.2011.71 errata
HOR 2010
Harald Zankl, Nao Hirokawa, and Aart Middeldorp.
Uncurrying for Innermost Termination and Derivational Complexity.
Proceedings of the 5th International Workshop on Higher-Order Rewriting, Electronic Proceedings in Theoretical Computer Science 49, pp. 46–57, 2011.
doi: 10.4204/EPTCS.49.4
IJCAR 2010
Nao Hirokawa and Aart Middeldorp.
Decreasing Diagrams and Relative Termination.
Proceedings of the 5th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 6173, pp. 487–501, 2010.
doi: 10.1007/978-3-642-14203-1_41
LPAR 2008
Nao Hirokawa and Georg Moser.
Complexity, Graphs, and the Dependency Pair Method.
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science 5330, pp. 652–666, 2008.
doi: 10.1007/978-3-540-89439-1_45 errata
LPAR 2008
Nao Hirokawa, Aart Middeldorp, and Harald Zankl.
Uncurrying for Termination.
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science 5330, pp. 667–681, 2008.
doi: 10.1007/978-3-540-89439-1_46
IJCAR 2008
Nao Hirokawa and Georg Moser.
Automated Complexity Analysis Based on the Dependency Pair Method.
Proceedings of the 4th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 5195, pp. 364–379, 2008.
doi: 10.1007/978-3-540-71070-7_32 errata
SOFSEM 2007
Harald Zankl, Nao Hirokawa, and Aart Middeldorp.
Constraints for Argument Filterings.
Proceedings of the 33rd International Conference on Current Trends in Theory and Practice of Computer Science, Lecture Notes in Computer Science 4362, pp. 579–590, 2006.
doi: 10.1007/978-3-540-69507-3_50
RTA 2006
Nao Hirokawa and Aart Middeldorp.
Predictive Labeling.
Proceedings of the 17th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 4098, pp. 313–327, 2006.
doi: 10.1007/11805618_24
RTA 2005
Nao Hirokawa and Aart Middeldorp.
Tyrolean Termination Tool.
Proceedings of the 16th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 3467, pp. 175–184, 2005.
doi: 10.1007/978-3-540-32033-3_14
AISC 2004
Nao Hirokawa and Aart Middeldorp.
Polynomial Interpretations with Negative Coefficients.
Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Mathematical Computation, Lecture Notes in Artificial Intelligence 3249, pp. 185–198, 2004.
doi: 10.1007/978-3-540-30210-0_16
RTA 2004
Nao Hirokawa and Aart Middeldorp.
Dependency Pairs Revisited.
Proceedings of the 15th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 3091, pp. 249–268, 2004.
doi: 10.1007/978-3-540-25979-4_18
CADE 2003
Nao Hirokawa and Aart Middeldorp.
Automating the Dependency Pair Method.
Proceedings of the 19th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 2741, pp. 32–46, 2003.
doi: 10.1007/978-3-540-45085-6_4 Thoralf Skolem Award
RTA 2003
Nao Hirokawa and Aart Middeldorp.
Tsukuba Termination Tool.
Proceedings of the 14th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 2706, pp. 311–320, 2003.
doi: 10.1007/3-540-44881-0_22 errata best paper award

Thesis

PhD 2006
Nao Hirokawa.
Automated Termination Analysis for Term Rewriting.
Ph.D. Thesis, University of Innsbruck, 2006.