Publication List
-
KUSAKARI Keiichirou,
Static Dependency Pair Method in Functional Programs,
IEICE Transactions on Information and Systems,
Vol.E101-D No.6, pp.1491-1502, Jun 2018.
[J-STAGE]
-
YAMADA Akihisa, Christian Sternagel, René Thiemann, KUSAKARI Keiichirou,
AC Dependency Pairs Revisited,
25th EACSL Annual Conference on Computer Science Logic (CSL 2016),
LIPIcs 62, pp.8:1-16, Aug 2016.
-
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki,
A Unified Ordering for Termination Proving,
Science of Computer Programming, 2014.
(In press, manuscript is available as
CoRR abs/1404.6245).
-
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki,
Nagoya Termination Tool,
In Proc. Joint 25th International Conference on Rewriting Techniques and Applications
and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
LNCS 8560, pp.466-475, Jul 2014.
-
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki,
Unifying the Knuth-Bendix, Recursive Path and Polynomial Orders,
In Proc. of 15th International Symposium on Principles and Practice of Declarative Programming (PPDP2013),
pp.181-192, 2013.
-
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki,
Partial Status for KBO,
In Proc. of 13th International Workshop on Termination (WST2013),
pp.74-78, 2013.
-
KUSAKARI Keiichirou,
Static Dependecy Pair Method in Rewriting Systems
for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types,
IEICE Transactions on Information and Systems,
Vol.E96-D, No.3, pp.472-480, Mar 2013.
[J-STAGE]
-
YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki, SAKAI Masahiko, NISHIDA Naoki,
A Sound Type System for Typing Runtime Errors,
IPSJ Transactions on Programming, Vol.5, No.2, pp.16-24, Mar 2012.
-
KOJIMA Yoshiharu, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki,
Decidability of Reachability for Right-Shallow Context-Sensitive Term Rewriting Systems,
IPSJ Transactions on Programming, Vol.4, No.4, pp.12-35, Sep 2011.
-
SUZUKI Sho, KUSAKARI Keiichirou, Frédéric Blanqui,
Argument Filterings and Usable Rules in Higher-Order Rewrite Systems,
IPSJ Transactions on Programming, Vol.4, No.2, pp.1-12, Mar 2011.
[J-STAGE]
-
NAKABAYASHI Naoki, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki, SAKAI Masahiko,
Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems,
Computer Software, Vol.28, No.1, pp.173-189, Feb 2011. (in Japanese)
-
UMANO Yohei, SAKAI Masahiko, NISHIDA Naoki, SAKABE Toshiki, KUSAKARI Keiichirou,
Solving Satisfiability of CNF Formulas with Clauses
Based on Elementary Symmetric Functions,
IEICE Transactions on Information and Systems,
Vol.J93-D, No.1, pp.1-9, Jan 2010.
-
KUSAKARI Keiichirou, ISOGAI Yasuo, SAKAI Masahiko, Frédéric Blanqui,
Static Dependency Pair Method based on Strong Computability
for Higher-Order Rewrite Systems,
IEICE Transactions on Information and Systems,
Vol.E92-D, No.10, pp.2007-2015, Oct 2009.
[J-STAGE]
-
KOJIMA Yoshiharu, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki,
Context-Sensitive Innermost Reachability is Decidable
for Linear Right-Shallow Term Rewriting Systems,
IPSJ Transactions on Programming, Vol.2, No.3, pp.20-32, Jul 2009.
-
SAKATA Tsubasa, NISHIDA Naoki, SAKABE Toshiki, SAKAI Masahiko, KUSAKARI Keiichirou,
Rewriting Induction for Constrained Term Rewriting Systems,
IPSJ Transactions on Programming,
Vol.2, No.2, pp.80-96, Mar 2009.
-
KUSAKARI Keiichirou, SAKAI Masahiko,
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques,
IEICE Transactions on Information and Systems,
Vol.E92-D, No.2, pp.235-247, Feb 2009.
[J-STAGE]
-
FURUICHI Yuuki, NISHIDA Naoki, SAKAI Masahiko, KUSAKARI Keiichirou, SAKABE Toshiki,
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, Sep 2008. (in Japanese)
-
KUROKAWA Sho, KUWABARA Hiroaki, YAMAMOTO Shinichiro,
SAKABE Toshiki, SAKAI Masahiko, KUSAKARI Keiichirou, Nishida Naoki,
A Type System for Analyzing Secure Information Flow
in Object-Oriented Programs with Exception Handling,
IEICE Transactions on Information and Systems,
Vol.J91-D, No.3, pp.757-770, Mar 2008. (in Japanese)
-
KUSAKARI Keiichirou, SAKAI Masahiko,
Enhancing Dependency Pair Method
using Strong Computability in Simply-Typed Term Rewriting,
Applicable Algebra in Engineering, Communication and Computing,
Vol.18, No.5, pp.407-431, Oct 2007.
[Springer]
-
KUSAKARI Keiichirou, CHIBA Yuki,
A Higher-Order Knuth-Bendix Procedure and its Applications,
IEICE Transactions on Information and Systems,
Vol.E90-D, No.4, pp.707-715, Apr 2007.
[PS/PDF]
-
SAKURAI Takahiro, KUSAKARI Keiichirou, SAKAI Masahiko, SAKABE Toshiki, NISHIDA Naoki,
Usable Rules and Labeling Product-Typed Terms
for Dependency Pair Method in Simply-Typed Term Rewriting Systems,
IEICE Transactions on Information and Systems,
Vol.J90-D, No.4, pp.978-989, Apr 2007. (in Japanese)
[PS/PDF]
-
KUSAKARI Keiichirou, NAKAMURA Masaki, TOYAMA Yoshihito,
Elimination Transformations
for Associative-Commutative Rewriting Systems,
Journal of Automated Reasoning, Vol.37, No.3, pp.205-229, Oct 2006.
[PS/PDF]
-
KUSAKARI Keiichirou, SAKAI Masahiko, SAKABE Toshiki,
Primitive Inductive Theorems Bridge
Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting,
IEICE Transactions on Information and Systems,
Vol.E88-D, No.12, pp.2715-2726, Dec 2005.
[PS/PDF]
-
SAKURAI Takahiro, KUSAKARI Keiichirou, NISHIDA Naoki, SAKAI Masahiko, SAKABE Toshiki,
Proving Sufficient Completeness of Functional Programs
based on Recursive Structure Analysis and Strong Computability,
In Proceedings of the Forum on Information Technology 2005 (FIT2005),
Information Technology Letters (LA-001), pp.1-4, Sep 2005. (in Japanese)
[PS/PDF]
-
SAKAI Masahiko, KUSAKARI Keiichirou,
On Dependency Pair Method for Proving Termination
of Higher-Order Rewrite Systems,
IEICE Transactions on Information and Systems,
Vol.E88-D, No.3, pp.583-593, Mar 2005.
[PDF]
-
NAGASHIMA Masanori, SAKAI Masahiko, SAKABE Toshiki, KUSAKARI Keiichirou,
Program Generation by Transformation from Quantified Equational Specifications,
Computer Software, Vol.21, No.4, pp.49-54, 2004. (in Japanese)
-
KUSAKARI Keiichirou,
Higher-Order Path Orders based on Computability,
IEICE Transactions on Information and Systems,
Vol.E87-D, No.2, pp.352-359, Feb 2004.
[PS/PDF]
-
M.Sakai and K.Kusakari,
On Proving Termination of Higher-Order Rewrite Systems
by Dependency Pair Technique,
The First International Workshop on Higher-Order Rewriting (HOR'02),
p.25, Jul 2002.
-
M.Sakai and K.Kusakari,
On New Dependency Pair Method for Proving Termination
of Higher-Order Rewrite Systems,
The International Workshop on Rewriting in Proof and Computation (RPC'01),
pp.176-187, Oct 2001.
-
K.Kusakari,
On Proving Termination of Term Rewriting Systems
with Higher-Order Variables,
IPSJ Transactions on Programming,
Vol.42, No.SIG 7 (PRO 11), pp.35-45, 2001.
[PS]
-
K.Kusakari, Y.Toyama,
On Proving AC-Termination by AC-Dependency Pairs,
IEICE Transactions on Information and Systems,
Vol.E84-D, No.5, pp.604-612, 2001.
[PS]
-
K.Kusakari, Y.Toyama,
On Proving AC-Termination by Argument Filtering Method,
IPSJ Transactions on Programming,
Vol.41, No.SIG 4 (PRO 7), pp.65-78, 2000.
[PS]
-
K.Kusakari,
Termination, AC-Termination and Dependency Pairs
of Term Rewriting Systems,
Ph.D. Thesis, JAIST, 2000.
[PS/PDF];
-
M.Nakamura, K.Kusakari, Y.Toyama,
On Proving Termination by General Dummy Elimination,
IEICE Transactions on Information and Systems,
Vol. J82-D-I, No.10, pp.1225-1231, 1999. (in Japanese)
-
K.Kusakari, M.Nakamura, Y.Toyama,
Argument Filtering Transformation,
In Proceedings of International Conference on
Principles and Practice of Declarative Programming,
LNCS 1702 (PPDP'99), pp.47-61, 1999.
[draft]
[Top Page]