Naoki Nishida.

*Transformational Approach to Inverse Computation in Term Rewriting*.

Doctor thesis, Nagoya University, Nagoya, Japan (2004-1).

[ps] [pdf]

Takahiro Nagao and Naoki Nishida.

**Rewriting induction for constrained inequalities**.

*Science of Computer Programming*, Vol. 155, pp. 76-102, April 2018.

[link]Naoki Nishida, Adrián Palacios, and Germán Vidal.

**Reversible computation in term rewriting**.

*Journal of Logical and Algebraic Methods in Programming*94:128-149, January 2018.

[link]Carsten Fuhs, Cynthia Kop, and Naoki Nishida.

**Verifying Procedural Programs via Constrained Rewriting Induction**.

*ACM Transactions on Computational Logic*(TOCL) 18(2):14:1-14:50, June 2017.

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]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]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]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]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]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]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]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]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).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]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])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]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]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).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]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).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).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).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]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).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).

Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal.

**CauDEr: A Causal-Consistent Reversible Debugger for Erlang**,

In*Proceedings of the 14th International Conference on Functional and Logic Programming (FLOPS 2018)*,

Vol. 10818 of*Lecture Notes in Computer Science*, pp. 247-263, May 2018.

[link]Shinnosuke Mizutani and Naoki Nishida.

**Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction**.

In*Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017)*,

*Electronic Proceedings in Theoretical Computer Science*, Vol. 265, pp. 35-51, Open Publishing Association, February 2018.

[link]Tomohiro Sasano, Naoki Nishida, Masahiko Sakai and Tomoya Ueyama.

**Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers**.

In*Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017)*,

*Electronic Proceedings in Theoretical Computer Science*, Vol. 265, pp. 82-97, Open Publishing Association, February 2018.

[link]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.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]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.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]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.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]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.

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.

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.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]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]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]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.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]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.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.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.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")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.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).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).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]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]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]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).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).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).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).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])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]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]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]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]

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).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).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).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).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).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).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).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).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]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]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]

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)