Update: Aug 23, 2017

Selected Publications


Thesis

  1. Naoki Nishida.
    Transformational Approach to Inverse Computation in Term Rewriting.
    Doctor thesis, Nagoya University, Nagoya, Japan (2004-1).
    [ps] [pdf]

Journal (refereed)

  1. Carsten Fuhs, Cynthia Kop, Naoki Nishida.
    Verifying Procedural Programs via Constrained Rewriting Induction.
    ACM Transactions on Computational Logic (TOCL) 18(2):14:1-14:50, June 2017.

  2. José Iborra, Naoki Nishida, Germán Vidal, and Akihisa Yamada.
    Relative Termination via Dependency Pairs.
    Journal of Automated Reasoning 58(3):391-411, Springer, March, 2017.
    [link]

  3. Naoki Nishida and Germán Vidal.
    A framework for computing finite SLD trees.
    The Journal of Logical and Algebraic Methods in Programming, Vol. 84, Issue 2, pp. 197-217, March 2015.
    [link]

  4. Naoki Nishida and Germán Vidal.
    Conversion to tail recursion in term rewriting.
    The Journal of Logic and Algebraic Programming, Vol. 83, Issue 1, pp. 53-63, January 2014.
    [link]

  5. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity.
    Logical Methods in Computer Science, Vol. 8, No. 3-4, pp. 1-49, (2012-8).
    SPECIAL ISSUE: Selected papers of the "22nd International Conference on Rewriting Techniques and Applications (RTA'11)".
    Preliminary version can be found in the proceedings of RTA 2011.
    [link]

  6. Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, and Naoki Nishida.
    A Sound Type System for Typing Runtime Errors.
    IPSJ Transactions on Programming, Vol. 5, No. 2, pp. 16-24, (2012-3).
    [link]

  7. Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe.
    Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems.
    IPSJ Transactions on Programming, Vol. 4, No. 4, pp. 12-35 (2011-9).
    [link]

  8. Naoki Nakabayashi, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe, and Masahiko Sakai.
    Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems.
    Computer Software, Vol. 28, No. 1, pp. 173-189, (2011-2). (in Japanese).
    [translated version will be found here]

  9. Naoki Nishida and Germán Vidal.
    Termination of Narrowing via Termination of Rewriting.
    Applicable Algebra in Engineering, Communication and Computing, Vol. 21, No. 3, pp. 177-225, (2010-05).
    [link]

  10. Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe and Keiichirou Kusakari.
    Solving Satisfiability of CNF Formulas with Clauses based on Elementary Symmetric Functions.
    the IEICE Transactions on Information and Systems,
    Vol. J93-D, No. 1, pp. 1-9, (2010-1). (in Japanese).

  11. Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe.
    Context-Sensitive Innermost Reachability is Decidable for Linear Right-Shallow Term Rewriting Systems.
    IPSJ Transactions on Programming, Vol. 2, No. 3, pp.20-32 (2009-7).
    [link]

  12. Naoki Nishida and Masahiko Sakai.
    Completion after Program Inversion of Injective Functions.
    Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'08),
    Vol. 237 of Electronic Notes in Theoretical Computer Science, pp. 39-56, (2009-4).
    (This is a revised version of the preproceeding at WRS'08.)
    [link] (full version [pdf])

  13. Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, and Keiichirou Kusakari.
    Rewriting Induction for Constrained Term Rewriting Systems.
    IPSJ Transactions on Programming, Vol. 2, No. 2, pp. 80-96, (2009-3). (in Japanese)..
    [translated version will be found here]
    [link]

  14. Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe.
    Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems.
    IPSJ Transactions on Programming, Vol. 1, No. 2, pp. 100-121, (2008-9). (in Japanese)..
    [translated version will be found here]
    [link]

  15. Sho Kurokawa, Hiroaki Kuwabara, Shinichirou Yamamoto, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida.
    A Type System for Analyzing Secure Information Flow in Object-Oriented Programs with Exception Handling.
    The IEICE Transactions on Information and Systems,
    Vol. J91-D, No. 3, pp. 757-770, (2008-3). (in Japanese).

  16. Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai.
    Transformation for Refining Unraveled Conditional Term Rewriting Systems.
    Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2006),
    Vol. 174 of Electronic Notes in Theoretical Computer Science, Issue 10, pp. 75-95 (2007-7).
    (This is a revised version of the preproceeding at WRS'06.)
    [link]

  17. Takahiro Sakurai, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida.
    Usable Rules and Labeling Product-Typed Terms for Dependency Pair Method in Simply-Typed Term Rewriting Systems.
    The IEICE Transactions on Information and Systems,
    Vol. J90-D, No. 4, pp. 978-989 (2007-4). (in Japanese).

  18. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Generation of Inverse Computation Programs of Constructor Term Rewriting Systems.
    The IEICE Transactions on Information and Systems,
    Vol. J88-D-I, No. 8, pp. 1171-1183 (2005-8). (in Japanese).

  19. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Improving Efficiency of Computation of Right-Linear Constructor Term Rewriting Systems with Extra Variables.
    Computer Software,
    Vol. 21, No. 3, pp. 40-47 (2004-5). (in Japanese).

  20. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Narrowing-Based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof.
    Functional and Constraint Logic Programming,
    Vol. 86 of Electronic Notes in Theoretical Computer Science, No. 3, pp. 1-18 (2003-11).
    (the revised version of the proceeding at WFLP'03)
    [link]

  21. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Computation Model of Term Rewriting Systems with Extra Variables.
    Computer Software,
    Vol. 20, No. 5, pp. 85-89 (2003-9). (in Japanese).

  22. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Generation of a TRS Implementing the Inverses of Pure Treeless Functions.
    Computer Software,
    Vol. 19, No. 1, pp. 29-33 (2002-1). (in Japanese).

Proceedings (refereed)

  1. Naoki Nishida, Adrián Palacios, and Germán Vidal.
    Towards Reversible Computation in Erlang.
    In Revised Selected Papers of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016),
    Vol. 10184 of Lecture Notes in Computer Science, pp. 259-274, July 2017.

  2. Ryota Nakayama, Naoki Nishida, and Masahiko Sakai.
    Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems.
    In Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016),
    Electronic Proceedings in Theoretical Computer Science, Vol. 235, pp. 62–77, Open Publishing Association, January 2017.
    [EPTCS page] [link]

  3. Naoki Nishida.
    Notes on Confluence of Ultra-WLL SDCTRSs via a Structure-Preserving Transformation.
    In Proceedings of the 5th International Workshop on Confluence (IWC 2016), pp. 60-64, September, 2016.

  4. Takahiro Nagao and Naoki Nishida.
    Proving inductive validity of constrained inequalities.
    In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), pp. 50-61, ACM, September, 2016.
    [link]

  5. Naoki Nishida, Adrián Palacios, and Germán Vidal.
    Reversible Term Rewriting in Practice.
    In Informal Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), pp. 77-85, June, 2016.

  6. Naoki Nishida, Adrián Palacios, and Germán Vidal.
    Reversible Term Rewriting.
    In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016),
    Leibniz International Proceedings in Informatics, Vol. 52, pp. 28:1-28:18, June, 2016.
    [LIPIcs page]

  7. Cynthia Kop and Naoki Nishida.
    Constrained Term Rewriting tooL.
    In Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20),
    Vol. 9450 of Lecture Notes in Computer Science, pp. 549-557, November 2015.

  8. Cynthia Kop and Naoki Nishida.
    Automatic Constrained Rewriting Induction towards Verifying Procedural Programs.
    In Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014),
    Vol. 8858 of Lecture Notes in Computer Science, pp. 334-353, November 2014.

  9. Naoki Nishida and Takumi Kataoka.
    On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants.
    Proceedings of the 14th International Workshop on Termination (WST 2014), 5 pages, July 2014.

  10. Karl Gmeiner and Naoki Nishida.
    Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems.
    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014),
    OpenAccess Series in Informatics (OASIcs), Vol. 40, pp. 3-14, July 2014.
    [OASIcs page]

  11. Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner.
    On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings.
    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014),
    OpenAccess Series in Informatics (OASIcs), Vol. 40, pp. 39-50, July 2014.
    [OASIcs page] [link]

  12. Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, and Naoki Nishida.
    Inverse Unfold Problem and Its Heuristic Solving.
    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014),
    OpenAccess Series in Informatics (OASIcs), Vol. 40, pp. 27-38, July 2014.
    [OASIcs page]

  13. Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner.
    On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation.
    Proceedings of the 3rd International Workshop on Confluence (IWC 2014), pp. 24-28, July 2014.

  14. Naoki Nishida, Masahiko Sakai, and Yasuhiro Nakano.
    On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms.
    Proceedings of the 2nd International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2013), Electronic Proceedings in Theoretical Computer Science, Vol. 134, pp. 1–10, October 2013.
    [link]

  15. Cynthia Kop and Naoki Nishida.
    Term Rewriting with Logical Constraints.
    In Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013),
    Vol. 8152 of Lecture Notes in Artificial Intelligence, pp. 343-358, September 2013.

  16. Naoki Nishida and Germán Vidal.
    A Finite Representation of the Narrowing Space.
    In Revised Selected Papers of the 23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013),
    Vol. 8901 of Lecture Notes in Computer Science, pp. 54-71, December 2014.

  17. Karl Gmeiner, Naoki Nishida, and Bernhard Gramlich.
    Proving Confluence of Conditional Term Rewriting Systems via Unravelings.
    In Proceedings of the 2nd International Workshop on Confluence (IWC 2013),
    pp. 35-39, June 2013.

  18. Minami Niwa, Naoki Nishida and Masahiko Sakai.
    Improving Determinization of Grammar Programs for Program Inversion.
    In Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012),
    Vol. 7844 of Lecture Notes in Computer Science, pp. 155-175, April 2013.
    (Presented at LOPSTR 2012 as "Extending Matching Operation in Grammar Program for Program Inversion")

  19. Naoki Nishida and Germán Vidal.
    Computing More Specific Versions of Conditional Rewriting Systems.
    In Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012),
    Vol. 7844 of Lecture Notes in Computer Science, pp. 137-154, April 2013.

  20. Naoki Nishida, Futoshi Nomura, Katsuhisa Kurahashi and Masahiko Sakai.
    Constrained Tree Automata and their Closure Properties.
    In Proceedings of the 1st International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2012), pp. 24-34, (2012-6).

  21. Naoki Nishida and Germán Vidal.
    More Specific Term Rewriting Systems.
    In Proceedings of the 21st International Workshop on Functional and (Constraint) Logic Programming (WFLP 2012), 15 pages, (2012-5).

  22. Tsubasa Sakata, Naoki Nishida, and Toshiki Sakabe.
    On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs.
    In Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2011),
    Vol. 6816 of Lecture Notes in Computer Science, pp. 138-155 (2011-7).
    [link]

  23. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity.
    In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
    Vol. 10 of LIPIcs, pp. 267-282 (2011-5).
    [link]

  24. Naoki Nishida and Germán Vidal.
    Program Inversion for Tail Recursive Functions.
    In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
    Vol. 10 of LIPIcs, pp. 283-298 (2011-5).
    [link]

  25. Naoki Nishida, Masahiko Sakai, and Tatsuya Hattori.
    On Disproving Termination of Constrained Term Rewriting Systems.
    In Proceedings of the 11th International Workshop on Termination (WST 2010),
    5 pages (2010-7).

  26. José Iborra, Naoki Nishida, and Germán Vidal.
    Goal-directed and Relative Dependency Pairs for Proving the Termination of Narrowing.
    In Danny De Schreye, editor, Postproceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009),
    Vol. 6037 of Lecture Notes in Computer Science, pp. 52-66, Springer (2010-4).

  27. Naoki Nishida and Masahiko Sakai.
    Proving Injectivity of Functions via Program Inversion in Term Rewriting.
    In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010),
    Vol. 6009 of Lecture Notes in Computer Science, pp. 288-303, Springer (2010-4).

  28. José Iborra, Naoki Nishida, and Germán Vidal.
    Improving the Termination Analysis of Narrowing in Left-Linear Constructor Systems.
    In Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009),
    9 pages, (2009-9).

  29. Naoki Nishida, Masahiko Sakai, and Terutoshi Kato.
    Convergent Term Rewriting Systems for Inverse Computation of Injective Functions.
    In Dieter Hofbauer and Alexander Serebrenik, editors, Proceedings of the 9th International Workshop on Termination (WST'07),
    pp. 77-81, (2007-6).
    (the full version is available from [pdf])

  30. Naoki Nishida and Koichi Miura.
    Dependency Graph Method for Proving Termination of Narrowing.
    In Alfons Geser and Harald Søndergaard, editors, Proceedings of the 8th International Workshop on Termination (WST'06),
    pp. 12-16, (2006-8).
    [pdf]

  31. Takahiro Sakurai, Keiichirou Kusakari, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Proving Sufficient Completeness of Functional Programs based on Recursive Structure Analysis and Strong Computability.
    In Proceedings of the Forum on Information Technology 2005,
    No. LA-001 in Information Technology Letters, pp. 1-4 (2005-9). (in Japanese).
    [pdf]

  32. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Partial Inversion of Constructor Term Rewriting Systems.
    In Jürgen Giesl, editor, Proceedings of the 16th International Conference on Rewriting Techniques and Applications,
    Vol. 3467 of Lecture Notes in Computer Science, pp. 264-278. Springer (2005-4).
    [link][ps][pdf]

  33. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    Generation of Inverse Term Rewriting Systems for Pure Treeless Functions.
    In Yoshihito Toyama, editor, Proceedings of the International Workshop on Rewriting in Proof and Computation (RPC'01),
    pp. 188-198, Sendai, Japan (2001-10).
    [ps][pdf]

Unrefereed

  1. Naoki Nakabayashi, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe, and Masahiko Sakai.
    Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems.
    In Proceedings of the 26th Conference of Japan Society for Software Science and Technology (JSSST),
    7B-2, pp.1-14 (2009-9) (in Japanese).

  2. Naoki Nishida, Tsubasa Sakata, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe.
    A Reduction Order for Orienting Equations in Theorem Proving of Constrained TRSs.
    IEICE Technical Report SS2008-20, the Institute of Electronics, Information and Communication Engineers, (2008-7).
    Vol. 108, No. 173, pp. 43-48 (in Japanese).

  3. Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, and Keiichirou Kusakari.
    On Rewriting Induction for Presburger-Constrained Term Rewriting Systems.
    IEICE Technical Report SS2008-1, the Institute of Electronics, Information and Communication Engineers, (2008-5).
    Vol. 108, No. 64, pp. 1-6 (in Japanese).

  4. Kiyotaka Mizuno, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, and Keiichirou Kusakari.
    A Sufficient Condition for Termination of Transformations from Equations to Rewrite Rules.
    IEICE Technical Report SS2007-61, the Institute of Electronics, Information and Communication Engineers (2008-3).
    Vol. 107, No. 505, pp. 25-30 (in Japanese).

  5. Satoru Kondo, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida.
    Extending program-generation system GeneSys for allowing negation in equational specifications.
    IEICE Technical Report SS2007-45, the Institute of Electronics, Information and Communication Engineers (2007-12).
    Vol. 107, No. 392, pp. 43-48 (in Japanese).

  6. Tomohiro Mizutani, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari.
    Proving Non-termination of Logic Programs by Detecting Loops in Derivation Trees.
    IEICE Technical Report SS2007-30, the Institute of Electronics, Information and Communication Engineers (2007-10).
    Vol. 107, No. 275, pp. 1-6 (in Japanese).

  7. Yuji Sasada, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari.
    Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting.
    IEICE Technical Report SS2007-17, the Institute of Electronics, Information and Communication Engineers (IEICE) (2007-8).
    Vol. 107, No. 176, pp. 7-12 (in Japanese).

  8. Toshiki Murata, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari.
    Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems.
    IEICE Technical Report SS2007-16, the Institute of Electronics, Information and Communication Engineers (IEICE) (2007-8).
    Vol. 107, No. 176, pp. 1-6 (in Japanese).

  9. Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe.
    Approach to Software Verification Based on Transformation from Procedural Programs to Rewrite Systems.
    IEICE Technical Report SS2006-41 (KBSE2006-17), the Institute of Electronics, Information and Communication Engineers (IEICE) (2006-10).
    Vol. 106, No. 324, pp. 7-12 (in Japanese).
    [pdf]

  10. Koichi Miura, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari.
    Transformation of Equational Rewriting Systems for Removing some Equations.
    IEICE Technical Report SS2006-14, the Institute of Electronics, Information and Communication Engineers (IEICE) (2006-6).
    Vol. 106, No. 120, pp. 7-12 (in Japanese).
    [pdf]

  11. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe.
    On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems.
    IEICE Technical Report SS2004-18, the Institute of Electronics, Information and Communication Engineers, (2004-8).
    Vol. 104, No. 243, pp. 25--30.
    [ps][pdf]

all publications
Sakai Lab. Graduate School of Informatics Dept. of Information Engineering Graduate School/School of Engineering Nagoya University
Produced by N.Nishida (nishida @ i.nagoya-u.ac.jp)