Narrowing-based simulation of term rewriting systems with extra variables. - Naoki Nishida 001; Masahiko Sakai; Toshiki Sakabe (WFLP, 2003)

Partial Inversion of Constructor Term Rewriting Systems. - Naoki Nishida 001; Masahiko Sakai; Toshiki Sakabe (RTA, 2005)

Transformation for Refining Unraveled Conditional Term Rewriting Systems. - Naoki Nishida 001; Tomohiro Mizutani; Masahiko Sakai (WRS@FLoC, 2006)

Completion after Program Inversion of Injective Functions. - Naoki Nishida 001; Masahiko Sakai (WRS@RTA, 2008)

Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing. - José Iborra; Naoki Nishida 001; Germán Vidal (LOPSTR, 2009)

Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems. - Yoshiharu Kojima; Masahiko Sakai; Naoki Nishida 001; Keiichirou Kusakari; Toshiki Sakabe (Inf. Media Technol., 2009)

Proving Injectivity of Functions via Program Inversion in Term Rewriting. - Naoki Nishida 001; Masahiko Sakai (FLOPS, 2010)

Termination of narrowing via termination of rewriting. - Naoki Nishida 001; Germán Vidal (Appl. Algebra Eng. Commun. Comput., 2010)

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity. - Naoki Nishida 001; Masahiko Sakai; Toshiki Sakabe (RTA, 2011)

Program Inversion for Tail Recursive Functions. - Naoki Nishida 001; Germán Vidal (RTA, 2011)

On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs. - Tsubasa Sakata; Naoki Nishida 001; Toshiki Sakabe (WFLP, 2011)

Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems. - Yoshiharu Kojima; Masahiko Sakai; Naoki Nishida 001; Keiichirou Kusakari; Toshiki Sakabe (Inf. Media Technol., 2011)

Computing More Specific Versions of Conditional Rewriting Systems. - Naoki Nishida 001; Germán Vidal (LOPSTR, 2012)

Improving Determinization of Grammar Programs for Program Inversion. - Minami Niwa; Naoki Nishida 001; Masahiko Sakai (LOPSTR, 2012)

Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity - Naoki Nishida 001; Masahiko Sakai; Toshiki Sakabe (Log. Methods Comput. Sci., 2012)

A Sound Type System for Typing Runtime Errors. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe; Masahiko Sakai; Naoki Nishida 001 (Inf. Media Technol., 2012)

Term Rewriting with Logical Constraints. - Cynthia Kop; Naoki Nishida 001 (FroCos, 2013)

A Finite Representation of the Narrowing Space. - Naoki Nishida 001; Germán Vidal (LOPSTR, 2013)

On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms. - Naoki Nishida 001; Masahiko Sakai; Yasuhiro Nakano (TTATT, 2013)

Automatic Constrained Rewriting Induction towards Verifying Procedural Programs. - Cynthia Kop; Naoki Nishida 001 (APLAS, 2014)

Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems. - Karl Gmeiner; Naoki Nishida 001 (WPTE@RTA/TLCA, 2014)

Inverse Unfold Problem and Its Heuristic Solving. - Masanori Nagashima; Tomofumi Kato; Masahiko Sakai; Naoki Nishida 001 (WPTE@RTA/TLCA, 2014)

On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings. - Naoki Nishida 001; Makishi Yanagisawa; Karl Gmeiner (WPTE@RTA/TLCA, 2014)

Towards Verifying Procedural Programs using Constrained Rewriting Induction. - Cynthia Kop; Naoki Nishida 001 (CoRR, 2014)

Conversion to tail recursion in term rewriting. - Naoki Nishida 001; Germán Vidal (J. Log. Algebraic Methods Program., 2014)

Confluence Competition 2015. - Takahito Aoto 001; Nao Hirokawa; Julian Nagele; Naoki Nishida 001; Harald Zankl (CADE, 2015)

Reducing Relative Termination to Dependency Pair Problems. - José Iborra; Naoki Nishida 001; Germán Vidal; Akihisa Yamada 002 (CADE, 2015)

Constrained Term Rewriting tooL. - Cynthia Kop; Naoki Nishida 001 (LPAR, 2015)

A framework for computing finite SLD trees. - Naoki Nishida 001; Germán Vidal (J. Log. Algebraic Methods Program., 2015)

A Reversible Semantics for Erlang. - Naoki Nishida 001; Adrián Palacios; Germán Vidal (LOPSTR, 2016)

Proving inductive validity of constrained inequalities. - Takahiro Nagao; Naoki Nishida 001 (PPDP, 2016)

Reversible Term Rewriting. - Naoki Nishida 001; Adrián Palacios; Germán Vidal (FSCD, 2016)

Towards Reversible Computation in Erlang. - Naoki Nishida 001; Adrián Palacios; Germán Vidal (CoRR, 2016)

Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems. - Ryota Nakayama; Naoki Nishida 001; Masahiko Sakai (WPTE@FSCD, 2016)

Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction. - Shinnosuke Mizutani; Naoki Nishida 001 (WPTE@FSCD, 2017)

Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers. - Tomohiro Sasano; Naoki Nishida 001; Masahiko Sakai; Tomoya Ueyama (WPTE@FSCD, 2017)

Relative Termination via Dependency Pairs. - José Iborra; Naoki Nishida 001; Germán Vidal; Akihisa Yamada 002 (J. Autom. Reason., 2017)

Verifying Procedural Programs via Constrained Rewriting Induction. - Carsten Fuhs; Cynthia Kop; Naoki Nishida 001 (ACM Trans. Comput. Log., 2017)

CauDEr: A Causal-Consistent Reversible Debugger for Erlang. - Ivan Lanese; Naoki Nishida 001; Adrián Palacios; Germán Vidal (FLOPS, 2018)

Confluence Competition 2018. - Takahito Aoto 001; Makoto Hamana; Nao Hirokawa; Aart Middeldorp; Julian Nagele; Naoki Nishida 001; Kiraku Shintani; Harald Zankl (FSCD, 2018)

Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems. - Naoki Nishida 001; Yuya Maeda (FSCD, 2018)

Loop Detection by Logically Constrained Term Rewriting. - Naoki Nishida 001; Sarah Winkler (VSTTE, 2018)

On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems. - Yoshiaki Kanazawa; Naoki Nishida 001 (WPTE@FSCD, 2018)

On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions. - Naoki Nishida 001; Yuya Maeda (WPTE@FSCD, 2018)

A theory of reversibility for Erlang. - Ivan Lanese; Naoki Nishida 001; Adrián Palacios; Germán Vidal (J. Log. Algebraic Methods Program., 2018)

Reversible computation in term rewriting. - Naoki Nishida 001; Adrián Palacios; Germán Vidal (J. Log. Algebraic Methods Program., 2018)

Rewriting induction for constrained inequalities. - Takahiro Nagao; Naoki Nishida 001 (Sci. Comput. Program., 2018)

Characterizing Compatible View Updates in Syntactic Bidirectionalization. - Naoki Nishida 001; Germán Vidal (RC, 2019)

ReverCSP: Time-Travelling in CSP Computations. - Carlos Galindo 002; Naoki Nishida 001; Josep Silva; Salvador Tamarit (RC, 2020)

A Case Study for Reversible Computing: Reversible Debugging of Concurrent Programs. - James Hoey; Ivan Lanese; Naoki Nishida 001; Irek Ulidowski; Germán Vidal (Selected Results of the COST Action IC1405, 2020)

Determinization of inverted grammar programs via context-free expressions. - Naoki Nishida 001; Minami Niwa (J. Log. Algebraic Methods Program., 2021)

Reversible CSP Computations. - Carlos Galindo 002; Naoki Nishida 001; Josep Silva; Salvador Tamarit (IEEE Trans. Parallel Distributed Syst., 2021)

On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs. - Shujun Zhang; Naoki Nishida 001 (FLOPS, 2022)

Transforming orthogonal inductive definition sets into confluent term rewrite systems. - Shujun Zhang; Naoki Nishida 001 (J. Log. Algebraic Methods Program., 2022)

From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting. - Misaki Kojima; Naoki Nishida 001 (PADL, 2023)

On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic. - Ayuka Matsumi; Naoki Nishida 001; Misaki Kojima; Donghoon Shin (CoRR, 2023)

Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. - Misaki Kojima; Naoki Nishida 001 (J. Log. Algebraic Methods Program., 2023)

Equational Theories and Validity for Logically Constrained Term Rewriting. - Takahito Aoto 001; Naoki Nishida 001; Jonas Schöpf (FSCD, 2024)

On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness. - Misaki Kojima; Naoki Nishida 001 (RP, 2024)

Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version). - Takahito Aoto 001; Naoki Nishida 001; Jonas Schöpf (CoRR, 2024)

A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations. - Misaki Kojima; Naoki Nishida 001 (J. Inf. Process., 2024)

Transforming concurrent programs with semaphores into logically constrained term rewrite systems. - Misaki Kojima; Naoki Nishida 001; Yutaka Matsubara (J. Log. Algebraic Methods Program., 2025)

Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms. - Naoki Nishida 001; Misaki Kojima; Takumi Kato (J. Log. Algebraic Methods Program., 2025)

A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems. - Naoki Nishida 001; Misaki Kojima; Ayuka Matsumi (J. Log. Algebraic Methods Program., 2025)

Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version). - Kanta Takahata; Jonas Schöpf; Naoki Nishida 001; Takahito Aoto 001 (CoRR, 2025)

Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version). - Naoki Nishida 001; Misaki Kojima; Yuto Nakamura (CoRR, 2025)

Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version). - Kanta Takahata; Jonas Schöpf; Naoki Nishida 001; Takahito Aoto 001 (CoRR, 2025)