General Information
Nao Hirokawa (associate professor)
Contact
 address:
 School of Information Science
Graduate School of Advanced Science and Technology
Japan Advanced Institute of Science and Technology
11 Asahidai, Nomi, Ishikawa, 9231292, Japan  office:
 I54a (on 5th floor of Information Science Building II)
 phone:
 +81761511277
 email:
 hirokawa@jaist.ac.jp
 research group:
 Hirokawa Laboratory
 research interests:
 computational models (term rewriting, automata, complexity analysis)
automated deduction (automated theorem proving, SAT/SMT solving)
Maxcomp and Moca Saigawa
Teaching
 term 12: I116: Fundamentals of Programming
 term 21: I217E: Functional Programming
Upcoming Events
 58th TRS Meeting, February 20  22, 2023, Niigata, Japan.

8th International
Conference on Formal Structures of Computation and Deduction, July 3  6,
2023, Rome, Italy.
abstract: January 30, 2023; paper: February 3, 2023
Research Activities
Steering Committee Member
 IWC (20112020)
 International Workshop on Confluence
 CoCo (20112018)
 Confluence Competition
 LCC (20152017)
 International Workshop on Logic and Computational Complexity
 FSCD (20152016)
 International Conference on Formal Structures of Computation and Deduction
 RTA (20142015)
 International Conference on Rewriting Techniques and Applications (RTA)
Program Committee Member
 FSCD 2023
 8th International Conference on Formal Structures of Computation and Deduction
 WRLA 2022
 14th International Workshop on Rewriting Logic and its Applications,
 CADE28
 28th International Conference on Automated Deduction
 PPL 2021
 23rd Workshop on Programming and Programming Languages
 LPAR23
 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
 FSCD 2020
 5th International Conference on Formal Structures of Computation and Deduction
 WRLA 2020
 13th International Workshop on Rewriting Logic and its Applications
 FLOPS 2020
 15th International Symposium on Functional and Logic Programming
 PPL 2020
 22nd Workshop on Programming and Programming Languages
 CADE27
 27th International Conference on Automated Deduction
 FSCD 2019
 4th International Conference on Formal Structures of Computation and Deduction
 DICEFOPARA 2017
 8th Workshop on Developments in Implicit Computational complExity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis
 ITP 2017
 8th International Conference on Interactive Theorem Proving
 FSCD 2016
 1st International Conference on Formal Structures of Computation and Deduction
 IWC 2016
 5th International Workshop on Confluence
 CADE25
 25th International Conference on Automated Deduction
 PEPM 2015
 Workshop on Partial Evaluation and Program Manipulation
 LCC 2015
 16th International Workshop on Logic and Computational Complexity, cochair
 PPL 2014
 16th Workshop on Programming and Programming Languages
 SCSS 2014
 6th International Symposium on Symbolic Computation in Software Science
 LPAR19
 19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning
 RTA 2013
 24th International Conference on Rewriting Techniques and Applications
 IWC 2013
 2nd International Workshop on Confluence, cochair
 DCM 2013
 9th International Workshop on Developments in Computational Models
 WST 2013
 13th International Workshop on Termination
 RTA 2012
 23rd International Conference on Rewriting Techniques and Applications
 IWC 2012
 1st International Workshop on Confluence, cochair
 WST 2012
 12th International Workshop on Termination
 DICE 2012
 3rd International Workshop on Developments in Implicit Complexity
Organization
 AJSW 2016
 4th Austria  Japan Summer Workshop on Term Rewriting
 JL 2014
 1st JAISTLORIA Workshop
 PR 2013
 3rd Workshop on Proof Theory and Rewriting
Memberships
 IFIP TC1
 IFIP Technical Committee 1 (Foundations of Computer Science), 2018
 IFIP WG 1.6
 IFIP Working Group 1.6 (Rewriting), 2014
Publications
Journal Articles
 LMCS 2019
 Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler.
Abstract Completion, Formalized
Journal of Logical Methods in Computer Science, 15(3):1:11:19, 2019.
doi: 10.23638/LMCS15(3:19)2019  TPLP 2016
 Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp.
ACKBO Revisited,
Theory and Practice of Logic Programming, 16(2):163188, 2016.  JAR 2013
 Nao Hirokawa, Aart Middeldorp, and Harald Zankl.
Uncurrying for Termination and Complexity,
Journal of Automated Reasoning 50(3):279315, 2013.
 JAR 2011
 Nao Hirokawa and Aart Middeldorp
Decreasing Diagrams and Relative Termination
Journal of Automated Reasoning 47(4):481501, 2011
 JAR 2009
 Harald Zankl, Nao Hirokawa, and Aart Middeldorp
KBO Orientability
Journal of Automated Reasoning 43(2):173201, 2009
 IC 2007
 Nao Hirokawa and Aart Middeldorp
Tyrolean Termination Tool: Techniques and Features
Information and Computation 205(4):474511, 2007
 IC 2005
 Nao Hirokawa and Aart Middeldorp
Automating the Dependency Pair Method
Information and Computation 199(1,2):172199, 2005
Conference and Workshop Papers
 FSCD 2022

Kiraku Shintani and Nao Hirokawa
Compositional Confluence Criteria
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics, 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 for Computation and Deduction, Leibniz International Proceedings in Informatics 195, pp. 2:12:9, 2021.
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 Computer Science 11716, pp. 319335, 2019.
doi: 10.1007/9783030294366_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 for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 32:132:5, 2018
 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. 346353, 2018
doi: 10.1007/9783319942056_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 for Computation and Deduction, Leibniz International Proceedings in Informatics 84, pp. 19:119:16, 2017.
 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. 101104, 2015.
 CADE 2015
 Kiraku Shintani and Nao Hirokawa
CoLL: A Confluence Tool for LeftLinear Term Rewrite Systems
Proceedings of the 25th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 9195, pp. 127136, 2015.
 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. 209222, 2015.
 RTATLCA 2014

Nao Hirokawa and Georg Moser
Automated Complexity Analysis Based on ContextSensitive Rewriting
Proceedings of 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. 257271, 2014.
 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. 292307, 2014.
 FLOPS 2014

Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
ACKBO Revisited
Proceedings of the 12th International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science 8475, pp. 319335, 2014.
 LPAR 2012

Dominik Klein and Nao Hirokawa
Confluence of NonLeftLinear 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. 258273, 2012.
 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. 7180, 2011.
In the above PDF numbers 2, 5, and 14 for K (on pages 7 and 9) were corrected to 1, 4, and 13, respectively.
 HOR 2010

Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Uncurrying for Innermost Termination and Derivational Complexity
Proceedings of the 5th International Workshop on HigherOrder Rewriting, Electronic Proceedings in Theoretical Computer Science 49, pp. 4657, 2011
 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. 487501, 2010
 LPAR 2008

Nao Hirokawa, Aart Middeldorp, and Harald Zankl
Uncurrying for Termination
Proceedings of the 15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science 5330, pp. 667681, 2008
 LPAR 2008

Nao Hirokawa and Georg Moser
Complexity, Graphs, and the Dependency Pair Method
Proceedings of the 15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Lecture Notes in Computer Science 5330, pp. 652666, 2008
errata
 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. 364379, 2008
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. 579590, 2007
 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. 313327, 2006
 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. 175184, 2005
 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. 185198, 2004
 RTA 2004

Nao Hirokawa and Aart Middeldorp
Dependency Pairs Revisited
Proceedings of the 15th International Conference on Rewriting Techniques and Applications, Aachen, Lecture Notes in Computer Science 3091, pp. 249268, 2004
 CADE 2003

Nao Hirokawa and Aart Middeldorp
Automating the Dependency Pair Method
Proceedings of the 19th International Conference on Automated Deduction, Miami, Lecture Notes in Artificial Intelligence 2741, pp. 3246, 2003
 RTA 2003

Nao Hirokawa and Aart Middeldorp
Tsukuba Termination Tool
Proceedings of the 14th International Conference on Rewriting Techniques and Applications, Valencia, Lecture Notes in Computer Science 2706, pp. 311320, 2003
errata
Thesis
 Ph.D.

Nao Hirokawa
Automated Termination Analysis for Term Rewriting
Ph.D. Thesis, University of Innsbruck, 2006
Software
 Maxcomp
 A completion tool, which automatically finds a complete term rewrite system for an equational system.
 Saigawa
 A confluence tool for term rewrite systems.
 TTT
 A termination tool for term rewrite systems. This tool is no longer maintained. Instead, I would recommend its more powerful successor TTT2.