Argument Filtering Transformation. - Keiichirou Kusakari; Masaki Nakamura 001; Yoshihito Toyama (PPDP, 1999)

Higher-Order Path Orders Based on Computability. - Keiichirou Kusakari (IEICE Trans. Inf. Syst., 2004)

Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting. - Keiichirou Kusakari; Masahiko Sakai; Toshiki Sakabe (IEICE Trans. Inf. Syst., 2005)

On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems. - Masahiko Sakai; Keiichirou Kusakari (IEICE Trans. Inf. Syst., 2005)

Elimination Transformations for Associative-Commutative Rewriting Systems. - Keiichirou Kusakari; Masaki Nakamura 001; Yoshihito Toyama (J. Autom. Reason., 2006)

Enhancing dependency pair method using strong computability in simply-typed term rewriting. - Keiichirou Kusakari; Masahiko Sakai (Appl. Algebra Eng. Commun. Comput., 2007)

A Higher-Order Knuth-Bendix Procedure and Its Applications. - Keiichirou Kusakari; Yuki Chiba (IEICE Trans. Inf. Syst., 2007)

Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems. - Keiichirou Kusakari; Yasuo Isogai; Masahiko Sakai; Frédéric Blanqui (IEICE Trans. Inf. Syst., 2009)

Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques. - Keiichirou Kusakari; Masahiko Sakai (IEICE Trans. Inf. Syst., 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)

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)

Argument Filterings and Usable Rules in Higher-order Rewrite Systems. - Sho Suzuki; Keiichirou Kusakari; Frédéric Blanqui (Inf. Media Technol., 2011)

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

Unifying the Knuth-Bendix, recursive path and polynomial orders. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe (PPDP, 2013)

Static Dependency Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types. - Keiichirou Kusakari (IEICE Trans. Inf. Syst., 2013)

Nagoya Termination Tool. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe (RTA-TLCA, 2014)

A unified ordering for termination proving. - Akihisa Yamada 002; Keiichirou Kusakari; Toshiki Sakabe (Sci. Comput. Program., 2015)

AC Dependency Pairs Revisited. - Akihisa Yamada 002; Christian Sternagel; René Thiemann; Keiichirou Kusakari (CSL, 2016)

Static Dependency Pair Method in Functional Programs. - Keiichirou Kusakari (IEICE Trans. Inf. Syst., 2018)