Nao Hirokawa

General Information

Nao Hirokawa (associate professor)

Contact

address: School of Information Science
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@jaist.ac.jp
research group: Ogawa-Terauchi-Hirokawa Laboratory
 
research interests: term rewriting (confluence, strategies, and complexity analysis)
Maxcomp   Saigawa
 
research activities: CADE-25   PEPM 2015   IFIP WG 1.6   IWC   RTA   TRS Meeting
PPL 2014   JL 2014   CoCo 2014   SCSS 2014
LPAR-19   RTA 2013   IWC 2013   CoCo 2013   DCM 2013   WST 2013   PR 2013
RTA 2012   IWC 2012   CoCo 2012   WST 2012   DICE 2012  

Laboratory Introduction

Teaching

Upcoming Events

Publications

Journal Articles

JAR 2013 Nao Hirokawa, Aart Middeldorp, and Harald Zankl
Uncurrying for Termination and Complexity
Journal of Automated Reasoning 50(3), pp. 279-315, 2013
 
JAR 2011 Nao Hirokawa and Aart Middeldorp
Decreasing Diagrams and Relative Termination
Journal of Automated Reasoning 47(4), pp. 481-501, 2011
 
JAR 2009 Harald Zankl, Nao Hirokawa, and Aart Middeldorp
KBO Orientability
Journal of Automated Reasoning 43(2), pp. 173-201, 2009
 
IC 2007 Nao Hirokawa and Aart Middeldorp
Tyrolean Termination Tool: Techniques and Features
Information and Computation 205(4), pp. 474-511, 2007
 
IC 2005 Nao Hirokawa and Aart Middeldorp
Automating the Dependency Pair Method
Information and Computation 199(1,2), pp. 172-199, 2005

Conference and Workshop Papers

RTA-TLCA 2014 Nao Hirokawa and Georg Moser
Automated Complexity Analysis Based on Context-Sensitive Rewriting
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
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, Leibnitz 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 Conference 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.