[ English | Japanese ]

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
1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan
office:
I-54a (on 5th floor of Information Science Building II)
phone:
+81-761-51-1277
email:
hirokawa
term rewriting
@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

Upcoming Events

Research Activities

Steering Committee Member

IWC (2011-2020)
International Workshop on Confluence
CoCo (2011-2018)
Confluence Competition
LCC (2015-2017)
International Workshop on Logic and Computational Complexity
FSCD (2015-2016)
International Conference on Formal Structures of Computation and Deduction
RTA (2014-2015)
International Conference on Rewriting Techniques and Applications (RTA)

Program Committee Member

LPAR-24
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
CADE-29
29th International Conference on Automated Deduction
FSCD 2023
8th International Conference on Formal Structures of Computation and Deduction
WRLA 2022
14th International Workshop on Rewriting Logic and its Applications,
CADE-28
28th International Conference on Automated Deduction
PPL 2021
23rd Workshop on Programming and Programming Languages
LPAR-23
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
CADE-27
27th International Conference on Automated Deduction
FSCD 2019
4th International Conference on Formal Structures of Computation and Deduction
DICE-FOPARA 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
CADE-25
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, co-chair
PPL 2014
16th Workshop on Programming and Programming Languages
SCSS 2014
6th International Symposium on Symbolic Computation in Software Science
LPAR-19
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, co-chair
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, co-chair
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 JAIST-LORIA 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:1-1:19, 2019.
doi: 10.23638/LMCS-15(3:19)2019   errata
 
TPLP 2016
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp.
AC-KBO Revisited,
Theory and Practice of Logic Programming, 16(2):163-188, 2016.
 
JAR 2013
Nao Hirokawa, Aart Middeldorp, and Harald Zankl.
Uncurrying for Termination and Complexity
Journal of Automated Reasoning 50(3):279-315, 2013.
 
JAR 2011
Nao Hirokawa and Aart Middeldorp
Decreasing Diagrams and Relative Termination
Journal of Automated Reasoning 47(4):481-501, 2011
 
JAR 2009
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
KBO Orientability
Journal of Automated Reasoning 43(2):173-201, 2009
 
IC 2007
Nao Hirokawa and Aart Middeldorp
Tyrolean Termination Tool: Techniques and Features
Information and Computation 205(4):474-511, 2007
 
IC 2005
Nao Hirokawa and Aart Middeldorp
Automating the Dependency Pair Method
Information and Computation 199(1,2):172-199, 2005

Conference and Workshop Papers

FSCD 2023
Nao Hirokawa and Aart Middeldorp
Hydra Battles and AC Termination
Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics, 2023.
doi: tba
 
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:1-2: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. 319-335, 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 for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 32:1-32: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. 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 for Computation and Deduction, Leibniz International Proceedings in Informatics 84, pp. 19:1--19: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. 101-104, 2015.
 
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.
 
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.
 
RTA-TLCA 2014
Nao Hirokawa and Georg Moser
Automated Complexity Analysis Based on Context-Sensitive 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. 257-271, 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. 292-307, 2014.
 
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.
 
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.
 
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.
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 Higher-Order Rewriting, Electronic Proceedings in Theoretical Computer Science 49, pp. 46-57, 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. 487-501, 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. 667-681, 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. 652-666, 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. 364-379, 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. 579-590, 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. 313-327, 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. 175-184, 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. 185-198, 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. 249-268, 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. 32-46, 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. 311-320, 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.