Publication List

Refereed Papers

  1. 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]
  2. 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.
  3. YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki,
    A Unified Ordering for Termination Proving,
    Science of Computer Programming, Sep 2014. (In press, manuscript is available as CoRR abs/1404.6245).
  4. 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.
  5. YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki,
    Unifying the Knuth-Bendix, Recursive Path and Polynomial Orders,
    In Proc. of the 15th International Symposium on Principles and Practice of Declarative Programming (PPDP2013), pp.181-192, Sep 2013.
  6. YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki,
    Partial Status for KBO,
    In Proc. of the 13th International Workshop on Termination (WST2013), pp.74-78, Aug 2013.
  7. 草刈圭一朗,
    静的依存対法 －再帰定義は定義か？－,
    第15回プログラミングおよび言語ワークショップ(PPL2013), Mar 2013.
  8. 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]
  9. 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.
  10. 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.
  11. 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]
  12. 中林直生, 西田直樹, 草刈圭一朗, 坂部俊樹, 酒井正彦,
    制約付き項書換え系の書換え帰納法における補題等式の自動生成法,
    コンピュータソフトウェア, Vol.28, No.1, pp.173-189, Feb 2011.
  13. 馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗,
    基本対称関数に基づく節をもつCNF論理式の充足可能性判定,
    IEICE Transactions on Information and Systems, Vol.J93-D, No.1, pp.1-9, Jan 2010.
  14. 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]
  15. 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.
  16. 坂田翼, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗,
    制約付き項書換え系における書換え帰納法,
    情報処理学会論文誌 プログラミング, Vol.2, No.2, pp.80-96, Mar 2009.
  17. 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]
  18. 古市祐樹, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み,
    情報処理学会論文誌 プログラミング, Vol.1, No.2, pp.100-121, Sep 2008.
  19. 黒川翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム,
    IEICE Transactions on Information and Systems, Vol.J91-D, No.3, pp.757-770, Mar 2008.
  20. 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]
  21. 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]
  22. 櫻井敬大, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    単純型項書き換え系上の依存対法における実効規則と直積型項へのラベル付け
    (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.
    [PS/PDF]
  23. 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]
  24. 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]
  25. 櫻井敬大, 草刈圭一朗, 西田直樹, 酒井正彦, 坂部俊樹,
    関数プログラムの再帰構造解析と強計算性に基づく十分完全性の証明法,
    第4回情報科学技術フォーラム(FIT2005), 情報科学技術レターズ (LA-001), pp.1-4, Sep 2005.
    [PS/PDF]
  26. 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]
  27. 長島正憲, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    限量子付き等式理論の変換に基づく仕様からのプログラム生成,
    コンピュータソフトウェア, Vol.21, No.4, pp.49-54, July 2004.
  28. 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]
  29. 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.
  30. 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.
  31. 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, Jul 2001.
    [PS]
  32. 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, May 2001.
    [PS]
  33. 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, Jun 2000.
    [PS]
  34. 中村正樹, 草刈圭一朗, 外山芳人,
    消去法による項書換え系の停止性判定について
    (On Proving Termination by General Dummy Elimination),
    電子情報通信学会論文誌, J82-D-I, No.10, pp.1225-1231, Oct 1999.
  35. K.Kusakari, M.Nakamura, Y.Toyama,
    Argument Filtering Transformation,
    In Proceedings of the International Conference on Principles and Practice of Declarative Programming, LNCS 1702 (PPDP'99), pp.47-61, Sep 1999.
    [PS]

Theses

  1. K.Kusakari,
    Termination, AC-Termination and Dependency Pairs of Term Rewriting Systems,
    Ph.D. Thesis, JAIST, Mar 2000.
    [PS/PDF];
  2. K.Kusakari,
    非線形項書換え系の合流性について,
    Master's Thesis, JAIST, Mar 1996.

Reports and Unrefereed Papers

  1. 尾前貴則, 草刈圭一朗, 山田晃久, 坂部俊樹,
    項書換え系の停止性証明のための重み付き経路順序の抽象化,
    Abstracting Weighted Path Orders for Proving Termination of Term Rewriting Systems,
    2014年度冬のLAシンポジウム, pp.E-2.1-E-2.8, Jan 2015.
    計算理論とアルゴリズムの新潮流, 京都大学数理解析研究所講究録, No.1941, pp.66-73, Apr 2015.
  2. Naoki Nagatsuka, Masahiko Sakai, Zankl Harald, Keiichirou Kusakari,
    Size Complexity of BDD Construction of Pseudo-Boolean Constraints in binary/mixed-radix Base Form,
    The 28th Annual Conference of the Japan Society of Artifical Intelligence (JSAI 2014), 1D4OS-11a-3, 4 pages, May 2014.
  3. 中野靖大, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗, 橋本健二,
    制約付き木オートマトンにおける不用な遷移規則の発見法について,
    Tech. Rep. of IEICE (SS2013-77), Vol.113, No.489, pp.31-36, Mar 2014.
  4. 杢谷孔皓, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    プログラム中のポインタに関する表明式を動的に検査するインタプリタの開発,
    平成25年度電気関係学会東海支部連合大会講演論文集, No.M4-7, p.1, Sep 2013.
  5. 東野惇一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    配列を含むプログラムの検証のための非線形不等式型ループ不変式の生成,
    平成25年度電気関係学会東海支部連合大会講演論文集, No.M4-6, p.1, Sep 2013.
  6. 松原穂波, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    カリー化を組み込んだ高階辞書式経路順序の設計,
    平成25年度電気関係学会東海支部連合大会講演論文集, No.M4-5, p.1, Sep 2013.
  7. 坂井利光, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田 直樹,
    等式集合の語問題から基底等式集合の語問題への帰着可能性について,
    平成25年度電気関係学会東海支部連合大会講演論文集, No.M4-4, p.1, Sep 2013.
  8. 神谷尚史, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    単純型付き項書換え系における帰納的定理自動証明の局所戦略について,
    平成25年度電気関係学会東海支部連合大会講演論文集, No.M4-3, p.1, Sep 2013.
  9. 片岡巧, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    手続き型プログラムから書換え系への変換における停止性をより保存するためのループ不変式の利用,
    平成25年度電気関係学会東海支部連合大会講演論文集, No.M2-6, p.1, Sep 2013.
  10. 栗木隆太朗, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗,
    幅優先探索型完備化手続きのErlangによる実装の並列実行の評価,
    平成25年度電気関係学会東海支部連合大会講演論文集, No.M2-5, p.1, Sep 2013.
  11. 加藤起騎, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    Malbolgeのワード長の拡大とそのプログラミング支援ツール,
    Tech. Rep. of IEICE (SS2013-25), Vol.113, No.159, pp.73-78, July 2013.
  12. 伏見政晃, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    整数解を導出するための単体法とゴモリーカットの合成について,
    Tech. Rep. of IEICE (SS2012-78), Vol.112, No.458, pp.109-114, Mar 2013.
  13. 安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    Malbolge低級アセンブリプログラミングにおける制御命令の配置設計のためのSATソルバの利用,
    Tech. Rep. of IEICE (SS2012-50), Vol.112, No.373, pp.25-30, Jan 2013.
  14. 中野靖大, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    制約付き項のインスタンスを受理する制約付き木オートマトンの構成法,
    Tech. Rep. of IEICE (SS2012-47), Vol.112, No.373, pp.7-12, Jan 2013.
  15. 安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    三値関数を実現するMalbolge命令列の発見のためのSATエンコーディング,
    Tech. Rep. of IEICE (SS2012-37), Vol.112, No.275, pp.7-12, Nov 2012.
  16. 中野靖大, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    制約付き項のインスタンスを受理する制約付き木オートマトンの構成について,
    平成24年度電気関係学会東海支部連合大会講演論文集, No.A4-4, p.1, Sep 2012.
  17. 倉田佳佑, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    単純型付き項書換え系の停止性証明におけるカリー化の利用,
    平成24年度電気関係学会東海支部連合大会講演論文集, No.A4-3, p.1, Sep 2012.
  18. 伏見政晃, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗,
    Cooperの限量子除去アルゴリズムと単体法を逐次合成するための論理式変換,
    平成24年度電気関係学会東海支部連合大会講演論文集, No.A4-2, p.1, Sep 2012.
  19. NIWA Minami, NISHIDA Naoki, SAKAI Masahiko, SAKABE Toshiki, KUSAKARI Keiichirou,
    On Extending Matching Operation in Grammar Programs for Program Inversion,
    Tech. Rep. of IEICE (SS2012-27), Vol.112, No.164, pp.103-108, Jul 2012.
  20. KUSAKARI Keiichirou,
    Static Dependecy Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types,
    Tech. Rep. of IEICE (SS2012-9), Vol.112, No.23, pp.49-54, May 2012.
  21. 安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    Malbolgeの高級アセンブリ言語への配列機能の追加,
    Tech. Rep. of IEICE (SS2012-8), Vol.112, No.23, pp.43-48, May 2012.
  22. 大井一展, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    高階書換え系における引数切り落とし関数の下での実効規則について,
    Tech. Rep. of IEICE (SS2011-49), Vol.111, No.406, pp.57-62, Jan 2012.
  23. 尾関朗, 草刈圭一朗, 坂田翼, 西田直樹, 酒井正彦, 坂部俊樹,
    単純型付き項書換え系における書換え帰納法について,
    Tech. Rep. of IEICE (SS2011-48), Vol.111, No.406, pp.51-56, Jan 2012.
  24. 坂井利光, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗,
    語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて,
    Tech. Rep. of IEICE (SS2011-47), Vol.111, No.406, pp.45-49, Jan 2012.
  25. 鈴木英一, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    関数呼び出しを持つプログラムの非線形ループ不変式の自動生成,
    Tech. Rep. of IEICE (SS2011-46), Vol.111, No.406, pp.39-44, Jan 2012.
  26. 日野善信, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み,
    Tech. Rep. of IEICE (SS2011-38), Vol.111, No.268, pp.67-72, Oct 2011.
  27. 高桑一也, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    制約付き項書換え系における木準同型写像を用いた関数等価性検証,
    日本ソフトウェア科学会第28回大会講演論文集, No. 7B-1, 12 pages, Sep 2011.
  28. 安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    Malbolgeの高級アセンブリ言語への加算命令の追加,
    日本ソフトウェア科学会第28回大会講演論文集, No.5A-3, 12 pages, Sep 2011.
  29. 坂田翼, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    多重文脈書換え帰納法における反証と補題追加,
    日本ソフトウェア科学会第28回大会講演論文集, No.1A-4, 12 pages, Sep 2011.
  30. 服部達哉, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    線形左シャロー項書換え系の停止性の決定可能性について,
    平成23年度電気関係学会東海支部連合大会講演論文集, No.H1-6, p.1, Sep 2011.
  31. 鈴木英一, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    関数呼び出しを持つプログラムの不変式の自動生成について,
    平成23年度電気関係学会東海支部連合大会講演論文集, No.H1-5, p.1, Sep 2011.
  32. 倉橋克尚, 酒井正彦, 西田直樹, 野村太志, 坂部俊樹, 草刈圭一朗,
    制約付き木オートマトンとその閉包性,
    Tree Automata with Constraints and their Closure-Properties,
    Tech. Rep. of IEICE (SS2010-63), Vol.110, No.458, pp.61-66, Mar 2011.
  33. 服部達哉, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹,
    順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について,
    On Non-Termination Proof of Right-Linear and Right-Shallow Term Rewriting Systems Based on Forward Narrowing,
    Tech. Rep. of IEICE (SS2010-44), Vol.110, No.336, pp.31-36, Dec 2010.
  34. 長坂哲, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    難解言語Malbolgeのチューリング完全性について,
    On Turing Completness of an Esoteric Language, Malbolge,
    Tech. Rep. of IEICE (SS2010-37), Vol.110, No.227, pp.55-60, Oct 2010.
  35. 馬場達也, 坂部俊樹, 西田直樹, 草刈圭一朗, 酒井正彦,
    等式理論を法とするDPLL遷移系について,
    On DPLL Transition Systems Modulo Equational Theories,
    Tech. Rep. of IEICE (SS2010-36), Vol.110, No.227, pp.49-54, Oct 2010.
  36. 高桑一也, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    制約付き項書換え系における関数の効率的な等価性検証,
    平成22年度電気関係学会東海支部連合大会講演論文集, No.D3-6, p.1, Sep 2010.
  37. 日野善信, 酒井正彦, 草刈圭一朗, 坂部俊樹, 西田直樹,
    カウンタ法に基づく基本対称節を持つCNF論理式のSATソルバ,
    平成22年度電気関係学会東海支部連合大会講演論文集, No.D3-5, p.1, Sep 2010.
  38. 馬場達也, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    等式理論を法とする抽象DPLL アルゴリズムの提案,
    平成22年度電気関係学会東海支部連合大会講演論文集, No.D3-4, p.1, Sep 2010.
  39. SUZUKI Sho, KUSAKARI Keiichirou, Frédéric Blanqui,
    Argument Filterings and Usable Rules in Higher-Order Rewrite Systems,
    Tech. Rep. of IEICE (SS2010-24), Vol.110, No.169, pp.47-52, Aug 2010.
  40. 長島正憲, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗,
    条件付き等式の変換に基づくプログラム生成,
    Program Generation Based on Transformation of Conditional Equations,
    Tech. Rep. of IEICE (SS2009-41), Vol.109, No.343, pp.37-42, Dec 2009.
  41. 御宿義勝, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    右線形右シャローな項書換え系における文脈依存停止性の決定可能性について,
    On Decidability of Context-Sensitive Termination for Right-Linear Right-Shallow Term Rewriting Systems,
    Tech. Rep. of IEICE (SS2009-40), Vol.109, No.343, pp.31-36, Dec 2009.
  42. 鈴木翔, 草刈圭一朗, 坂部俊樹, 酒井正彦, 西田直樹,
    高階書換え系における引数切り落とし法と実効規則,
    Argument Filtering and Usable Rules in Higher-Order Rewrite Systems,
    Tech. Rep. of IEICE (SS2009-39), Vol.109, No.343, pp.25-30, Dec 2009.
  43. 中林直生, 西田直樹, 草刈圭一朗, 坂部俊樹, 酒井正彦,
    制約付き項書換え系の書換え帰納法における補題等式の自動生成法,
    Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems,
    日本ソフトウェア科学会第26回大会講演論文集, 7B-2, p.14, Sep 2009.
  44. 西田直樹, 中林直生, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    制約付き等式の定理自動証明器の試作,
    日本ソフトウェア科学会第26回大会講演論文集, 5P-4 (ポスター・デモ発表), Sep 2009.
  45. KOJIMA Yoshiharu, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki,
    Context-Sensitive Innermost Reduction of Linear Right-Shallow Term Rewriting Systems Effectively Preserves Regularity,
    LA-Symposium 2009 (Summer), pp.14.1-14.8, Jul 2009.
  46. UCHIYAMA Keita, SAKAI Masahiko, SAKABE Toshiki, KUSAKARI Keiichirou, NISHIDA Naoki,
    Decidability of Termination Properties for Term Rewriting Systems Consisting of Shallow Dependency Pairs,
    Tech. Rep. of IEICE (SS2008-45), Vol.108, No.362, pp.37-42, Dec 2008.
  47. 馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗,
    基本対称関数を付加したCNF論理式の充足可能性判定,
    Solving Satisfiability of CNF Formulas with Elementary Symmetric Functions,
    Tech. Rep. of IEICE (SS2008-44), Vol.108, No.362, pp.31-36, Dec 2008.
  48. 鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹,
    ビットエラー通信路におけるスケーラブルCANの動作解析,
    Behavior Analysis of Scalable CAN Protocol on a Bit-Error Channel,
    Tech. Rep. of IEICE (SS2008-37), Vol.108, No.242, pp.61-66, Oct 2008.
  49. 鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹,
    スケーラブルCANプロトコルの動作解析に関する予備的考察,
    平成20年度電気関係学会東海支部連合大会講演論文集, No.O-262, p.1, Sep 2008.
  50. 西田直樹, 坂田翼, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序,
    A Reduction Order for Orienting Equations in Theorem Proving of Constrained TRSs,
    Tech. Rep. of IEICE (SS2008-20), Vol.108, No.173, pp.43-48, Jul 2008.
  51. 坂田翼, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗,
    プレスブルガー文付き項書換え系における書換え帰納法について,
    On Rewriting Induction for Presburger-Constrained Term Rewriting Systems,
    Tech. Rep. of IEICE (SS2008-1), Vol.108, No.64, pp.1-6, May 2008.
  52. 水野清貴, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗,
    等式を規則化する変換の停止条件,
    A Sufficient Condition for Termination of Transformations from Equations to Rewrite Rules,
    Tech. Rep. of IEICE (SS2007-62), Vol.107, No.505, pp.31-36, Mar 2008.
  53. KUSAKARI Keiichirou, SAKAI Masahiko,
    Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques,
    Tech. Rep. of IEICE (SS2007-61), Vol.107, No.505, pp.25-30, Mar 2008.
  54. YAMADA Akihisa, KUSAKARI Keiichirou, SAKAI Masahiko, SAKABE Toshiki, NISHIDA Naoki,
    Error Detection with Soft Typing for Dynamically Typed Languages,
    Tech. Rep. of IEICE (SS2007-59), Vol.107, No.505, pp.13-18, Mar 2008.
  55. 馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗,
    対話型埋込みによる数独問題の設計ツール,
    A Tool for Designing Sudoku Problems by Interactive Fill-in Approach,
    Tech. Rep. of IEICE (SS2007-50), Vol.107, No.392, pp.73-78, Dec 2007.
  56. 近藤悟, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    プログラム生成系GeneSysにおける等式仕様への否定の導入,
    Extending Program-Generation System GeneSys for Allowing Negation in Equational Specifications,
    Tech. Rep. of IEICE (SS2007-45), Vol.107, No.392, pp.43-48, Dec 2007.
  57. 水谷知博, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    導出木からのループ検出による論理プログラムの非停止性証明法,
    Proving Non-termination of Logic Programs by Detecting Loops in Derivation Trees,
    Tech. Rep. of IEICE (SS2007-30), Vol.107, No.275, pp.1-6, Oct 2007.
  58. 伊藤寛之, 酒井正彦, 草刈圭一朗, 坂部俊樹, 西田直樹,
    論理式への変換に基づく魔方陣の発見,
    平成19年度電気関係学会東海支部連合大会講演論文集, p.O-012, Sep 2007.
  59. 笹田悠司, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗,
    振舞等価性の証明のための等式付き書換えに基づく潜在帰納法,
    Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting,
    Tech. Rep. of IEICE (SS2007-17), Vol.107, No.176, pp.7-12, Aug 2007.
  60. 村田俊樹, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン,
    Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems,
    Tech. Rep. of IEICE (SS2007-16), Vol.107, No.176, pp.1-6, Aug 2007.
  61. 磯谷泰巨, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    二階の書換え系における引数切り落とし法,
    Argument Filtering Method on Second-Order Rewriting System,
    Tech. Rep. of IEICE (SS2007-13), Vol.107, No.99, pp.23-28, Jun 2007.
  62. KUSAKARI Keiichirou, ISOGAI Yasuo, SAKAI Masahiko, SAKABE Toshiki, NISHIDA Naoki,
    Static Dependeycy Pair Method for Proving Termination of Higher-Order Rewriting Systems,
    Tech. Rep. of IEICE (SS2007-12), Vol.107, No.99, pp.17-22, Jun 2007.
  63. Yi Wang, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari,
    Confluence of Length Preserving String Rewriting System is Undecidable,
    京都大学数理解析研究所講究録, 計算機科学の理論とその応用
    (In RIMS Kokyuroku, Theory of Computer Science and Its Applications), Vol.1554, pp.171-177, May 2007.
    (LA-Symposium 2006 Winter, pp.27.1-27.6, Jan 2007.)
  64. Keita Uchiyama, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari,
    Decidability of Innermost Termination for Semi-Constructor Term Rewriting Systems,
    京都大学数理解析研究所講究録, 計算機科学の理論とその応用
    (In RIMS Kokyuroku, Theory of Computer Science and Its Applications), Vol.1554, pp.166-170, May 2007.
    (LA-Symposium 2006 Winter, pp.26.1-26.4, Jan 2007.)
  65. 蒲田明憲, 草刈圭一朗, 西田直樹, 酒井正彦, 坂部俊樹,
    単純型項書換え系における定理自動証明系HOPSYS,
    Automated Theorem Prover HOPSYS on Simply-Typed Rewriting Systems,
    Tech. Rep. of IEICE (SS2006-57), Vol.106, No.426, pp.7-12, Dec 2006.
  66. NISHIDA Naoki, FURUICHI Yuki, SAKAI Masahiko, KUSAKARI Keiichirou, SAKABE Toshiki,
    Software Verification Based on Transformation from Procedural Programs to Rewrite Systems,
    In Proceedings of the 4th Symposium on Intelligent Media Integration for Social Information Infrastructure (COE-IMI), pp.129-130, Dec 2006.
  67. 近藤悟, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗,
    GeneSysによるプログラム生成例とIntroduction規則の追加,
    Example programs generated by GeneSys and proposal of Introduction rule,
    Tech. Rep. of IEICE (SS2006-46), Vol.106, No.324, pp.37-42, Oct 2006.
  68. 黒川翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    例外処理付きオブジェクト指向言語における情報流の安全性解析,
    Security Analysis of Information Flow for an Object-Oriented Language with Exception Handling,
    Tech. Rep. of IEICE (SS2006-42), Vol.106, No.324, pp.13-18, Oct 2006.
  69. 古市祐樹, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み,
    Approach to Software Verification Based on Transforming from Procedural Programs to Rewrite Systems,
    Tech. Rep. of IEICE (SS2006-41), Vol.106, No.324, pp.7-12, Oct 2006.
  70. 村田俊樹, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    所属制約を持つ条件付き項書換え系の紐解き変換,
    平成18年度電気関係学会東海支部連合大会論文集, No.O-438, p.1, Sep 2006.
  71. 笹田悠司, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    高階関数機能を持つ項書換え系のコンパイル,
    平成18年度電気関係学会東海支部連合大会論文集, No.O-437, p.1, Sep 2006.
  72. 櫻井敬大, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け,
    Usable Rules and Labeling Product-Typed Term for Dependency Pair Method in Simply-Typed Term Rewriting Systems,
    Tech. Rep. of IEICE (SS2006-15), Vol.106, No.120, pp.13-18, Jun 2006.
  73. 三浦浩一, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    等式付き書換え系の等式数を削減する変換,
    Transformation of Equational Rewriting Systems for Removing Some Equations,
    Tech. Rep. of IEICE (SS2006-14), Vol.106, No.120, pp.7-12, Jun 2006.
  74. 水谷知博, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    紐解かれた項書換え系の文脈依存条件の除去のための変換,
    Transformation for Removing Context-Sensitivity of TRSs Obtained by Unraveling,
    In RIMS Kokyuroku, New Aspects of Theoretical Computer Science, Vol.1489, pp.195-201, May 2006.
    (LA-Symposium 2005 Winter, pp.30.1-30.6, Jan 2006.)
  75. 磯谷泰巨, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    強計算依存対法による高階書換え系の停止性証明,
    Proving Termination of Higher-Order Rewrite Systems based on Strongly Computable Dependency Pair Method,
    Tech. Rep. of IEICE (SS2006-6), Vol.106, No.15, pp.31-36, Apr 2006.
  76. 星野由美, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹,
    関数プログラムの停止性証明に関する辞書式経路順序,
    Lexicographic Path Ordering for Proving Termination of Functional Programs,
    Tech. Rep. of IEICE (SS2005-85), Vol.105, No.597, pp.13-18, Feb 2006.
  77. 田代善彦, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    項正規表現に基づくSpi計算の機密性検証,
    Secrecy Verification of Spi Calculus based on Term Regular Expressions,
    Tech. Rep. of IEICE (SS2005-82), Vol.105, No.596, pp.35-40, Feb 2006.
  78. WANG Yi, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki,
    Decidability of Termination for Left-Linear Shallow Term Rewriting Systems and Related,
    Tech. Rep. of IEICE (COMP2005-50), Vol.105, No.499, pp.9-13, Dec 2005.
  79. 佐伯昌樹, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    分散JoinJAVAプログラムの通信エラーに対する型判定システム,
    Type Judgement System for Communication Error in Distributed JoinJAVA Programs,
    Tech. Rep. of IEICE (SS2005-67), Vol.105, No.491, pp.25-30, Dec 2005.
  80. 草刈圭一朗, 酒井正彦,
    強計算性による単純型項書換え系の依存対法の改良,
    Enhancing Dependency Pair Method by Strong Computability in Simply-Typed Term Rewriting Systems,
    Tech. Rep. of IEICE (SS2005-65), Vol.105, No.491, pp.13-18, Dec 2005.
  81. 奥谷大介, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    暗号プロトコル記述からカラーペトリネットへの変換による機密性検証,
    Secrecy Verification by Transforming Cryptographic Protocol Descripstions to Coloured Petri Nets,
    Tech. Rep. of IEICE (SS2005-58), Vol.105, No.490, pp.19-24, Dec 2005.
  82. 岩田篤史, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹,
    重なりを持つTRSにおける最外戦略の完全性について,
    On Completeness of Outermost Strategy for Overlapping TRSs,
    Tech. Rep. of IEICE (SS2005-46), Vol.105, No.331, pp.39-44, Oct 2005.
  83. Yi Wang, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe,
    Decidability of Termination for Semi-Constructor Term Rewriting Systems,
    Tech. Rep. of IEICE (SS2005-26), Vol.105, No.228, pp.13-18, Aug 2005.
  84. 三浦浩一, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    ナローイング計算の停止性証明のための依存グラフ法,
    Dependency Graph Method for Proving Termination of Narrowing,
    Tech. Rep. of IEICE (SS2005-23), Vol.105, No.129, pp.31-36, Jun 2005.
  85. 飯澤恒, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹,
    難読プログラミング言語Malbolgeにおけるプログラム構成手法,
    Programming Method in Obfuscated Language Malbolge,
    Tech. Rep. of IEICE (SS2005-22), Vol.105, No.129, pp.25-30, Jun 2005.
  86. 草刈圭一朗, 櫻井敬大, 西田直樹, 酒井正彦, 坂部俊樹,
    強計算性に基づいた単純型項書換え系の停止性証明法,
    On Proving Termination of Simply-Typed Term Rewriting Systems Based on Strong Computability,
    Tech. Rep. of IEICE (SS2005-21), Vol.105, No.129, pp.19-24, Jun 2005.
  87. 岡本晃治, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹,
    弱最内戦略を完全にする項書換え系の等価変換,
    In RIMS Kokyuroku, Theoretical Computer Science and its Applications, Vol.1426, pp.119-125, Apr 2005.
    (LA-Symposium 2004 Winter, pp.21.1-21.8, Feb 2005.)
  88. 蛸島洋明, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗,
    変換と部分評価に基づく非左辺正規なメタ項の停止性証明,
    In RIMS Kokyuroku, Theoretical Computer Science and its Applications, Vol.1426, pp.113-118, Apr 2005.
    (LA-Symposium 2004 Winter, pp.20.1-20.6, Feb 2005.)
  89. 村田龍彦, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹,
    項到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係,
    In RIMS Kokyuroku, Theoretical Computer Science and its Applications, Vol.1426, pp.106-112, Apr 2005.
    (LA-Symposium 2004 Winter, pp.19.1-19.6, Feb 2005.)
  90. 高須洋平, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹,
    配列を扱う非線形先頭再帰プログラムからの再帰除去,
    On Recursion Removal from Non-Linear Top-Recursive Programs,
    In RIMS Kokyuroku, Theoretical Computer Science and its Applications, Vol.1426, pp.39-44, Apr 2005.
    (LA-Symposium 2004 Winter, pp.7.1-7.6, Feb 2005.)
  91. 長島正憲, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗,
    融合変換を模倣するプログラム生成変換の戦略,
    Simulating Fusion Transformation by Program-Generation Transformation,
    電子情報通信学会技術研究報告(SS2004-33), Vol.104, No.466, pp.43-48, Nov 2004.
  92. 岩田篤司, 草刈圭一朗, 酒井正彦, 坂部俊樹,
    項の全正規形を探索するためのTRSコンパイラ,
    平成16年度 電気関係学会東海支部連合大会, O-363, Sep 2004.
  93. 奥谷大介, 草刈圭一朗, 酒井正彦, 坂部俊樹,
    項書換え系と木オートマトンを用いた共通鍵方式暗号プロトコルの検証法,
    平成16年度 電気関係学会東海支部連合大会, O-352, Sep 2004.
  94. KUSAKARI Keiichirou, CHIBA Yuki,
    Higher-Order Knuth-Bendix Procedure and its Applications,
    LA-Symposium 2004 (Summer), pp.9.1-9.12, Jul 2004.
  95. KUSAKARI Keiichirou, SAKAI Masahiko, SAKABE Toshiki,
    Characterizing, Proving and Disproving Inductive Theorems in Higher-Order Rewriting,
    LA-Symposium 2004 (Summer), pp.8.1-8.11, Jul 2004.
  96. 水野健一, 草刈圭一朗, 酒井正彦, 坂部俊樹,
    左辺が一致するオーバレイ性を持つ左線形TRSの正規化戦略,
    2003年度冬のLAシンポジウム, pp.37.1-37.6, Feb 2004.
    計算機科学基礎理論の新展開, 京都大学数理解析研究所講究録, No.1375, pp.247-252, 2004.
  97. 山本友和,草刈圭一朗,酒井正彦,坂部俊樹,
    非完全な仕様における振舞等価性の自動証明法,
    Tech. Rep. of IEICE, COMP2003-66, pp.29-36, Dec 2003.
  98. K.Kusakari, M.Sakai, T.Sakabe,
    Characterizing Inductive Theorems by Extensional Initial Models in a Higher-Order Equational Logic,
    情報処理学会 第46回 プログラミング研究会 (46-9), Oct 2003.
  99. 長島正憲, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    限量子付き等式理論の変換に基づく仕様からのプログラム生成,
    日本ソフトウェア科学会 第20回全国大会, pp.431-435, Sep 2003.
  100. 千葉勇輝, 草刈圭一朗, 外山芳人,
    高階書き換え系に基づく完備化手続き,
    電気関係学会東北支部連合大会 平成15年度 1G-02, p.226, Aug 2003.
  101. 長島正憲, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    限量子付き等式理論からTRSへの被覆集合に基づく変換,
    2003年度夏のLAシンポジウム, pp.27.1-27.4, Jul 2003.
  102. 鶴川敏孝,草刈圭一朗,外山芳人,
    変換パターンに基づく高階プログラム変換,
    Tech. Rep. of IEICE, COMP2002-83 (2003-3), pp.61-68, Mar 2003.
  103. 伊藤芳浩,草刈圭一朗,外山芳人,
    完備化手続きによるプログラム融合変換の停止条件,
    Tech. Rep. of IEICE, COMP2002-84 (2003-3), pp.69-76, Mar 2003.
  104. 鶴川敏孝, 草刈圭一朗, 外山芳人,
    変換パターンに基づく高階プログラム変換,
    電気関係学会東北支部連合大会, 平成14年度 2D-11, p.141, Aug 2002.
  105. 伊藤芳浩, 草刈圭一朗, 外山芳人,
    完備化手続きによるプログラム融合変換の停止条件,
    電気関係学会東北支部連合大会, 平成14年度 2D-10, p.140, Aug 2002.
  106. 秋谷賢司, 草刈圭一朗, 外山芳人,
    項書き換え系の高速実行と柔軟実行の融合,
    電気関係学会東北支部連合大会, 平成14年度 2D-09, p.139, Aug 2002.
  107. Keiichirou Kusakari, Claude Marché, and Xavier Urbain,
    Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria,
    Research Report 1304, LRI, 2002.
  108. K.Kusakari,
    Path Orders in Simply-Typed Term Rewriting Systems,
    第14回情報基礎理論ワークショップ (LA Symposium 2001), pp.19.1-19.8, Jul 2001.
  109. K.Kusakari, Y.Toyama,
    Designing a Weak AC-Reduction Pair by Argument Filtering Method,
    第12回情報基礎理論ワークショップ (LA Symposium '99), pp.12.1-12.6, Jul 1999.
  110. K.Kusakari, M.Nakamura, Y.Toyama,
    Argument Filtering Transformation,
    Res. Rep. IS-RR-99-0008F, School of Information Science, JAIST, Mar 1999.
  111. K.Kusakari, Y.Toyama,
    The Hierarchy of Dependency Pairs,
    Res. Rep. IS-RR-99-0007F, School of Information Science, JAIST, Mar 1999.
  112. K.Kusakari, Y.Toyama,
    On Proving AC-Termination by Argument Filtering Method,
    Res. Rep. IS-RR-99-0006F, School of Information Science, JAIST, Mar 1999.
  113. K.Kusakari, Y.Toyama,
    On Proving Termination of Term Rewriting Systems by Pruning Method,
    Tech. Rep. of IEICE, COMP98-432(1998-11), pp.49-56, Nov 1998.
  114. K.Kusakari, Y.Toyama,
    On Proving AC-Termination by AC-Dependency Pairs,
    Res. Rep. IS-RR-98-0026F, School of Information Science, JAIST, Oct 1998.
  115. K.Kusakari, Y.Toyama,
    On Proving AC-Termination by Dependency Pairs,
    Tech. Rep. of IEICE, COMP97-112(1998-03), pp.47-54, Mar 1998.
  116. K.Kusakari, Y.Toyama,
    Designing a Termination Prover for Term Rewriting Systems,
    日本ソフトウェア科学会 第14回全国大会, pp.361-364, Sep 1997.
  117. K.Kusakari, M.Sakai, Y.Toyama,
    Church-Rosser Property of Finite Ranked Terms of Non-Linear Term Rewriting Systems,
    第9回情報基礎理論ワークショップ (LA Symposium '96), pp.160-165, Jul 1996.
  118. K.Kusakari, M.Sakai, Y.Toyama,
    Church-Rosser Property of Non-Linear Term Rewriting Systems,
    Tech. Rep. of IEICE, COMP95-86(1996-01), pp.123-129, Jan 1996 (in Japanese).
  119. 草刈 圭一朗, 酒井 正彦, 外山芳人,
    非線型項書換え系の合流性について,
    電気関係学会 北陸支部連合大会, 平成7年度 E-26, p.312, Sep 1995.

Presentations

  1. 草刈圭一朗, 横井雅也,
    二部グラフ上の屋島ゲームにおける局面値の特定,
    第7回日本組合せゲーム理論研究集会, Aug 2023.
  2. 草刈圭一朗,
    関数型プログラムの静的な再帰構造解析に基づく停止性証明手法,
    岐阜数理科学セミナー, July 2022.
  3. 安藤聡, 長坂哲, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    難解言語 Malbolge における高級アセンブリ言語への加算命令の追加,
    第13回プログラミングおよびプログラミング言語ワークショップ PPL2011, 論文集 p.214 (ポスター・デモ発表), Mar 2011.
  4. 長坂哲, 安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹,
    難解言語 Malbolge におけるプログラミング環境の構築と改良,
    第13回プログラミングおよびプログラミング言語ワークショップ PPL2011, 論文集 p.214 (ポスター・デモ発表), Mar 2011.
  5. 高桑一也, 西田直樹, 大場康司, 酒井正彦, 坂部俊樹, 草刈圭一朗,
    制約付き項書換え系における木準同型写像を用いた等価性証明ツール,
    第13回プログラミングおよびプログラミング言語ワークショップ PPL2011, 論文集 p.214 (ポスター・デモ発表), Mar 2011.
  6. 長坂哲, 伊藤寛之, 酒井正彦, 草刈圭一朗, 西田直樹, 坂部俊樹,
    SATソルバを利用したお絵かきロジックの問題作成支援ツール,
    組合せゲーム・パズルミニプロジェクト 第5回ミニ研究集会, Mar 2010.
  7. 馬場正貴, 酒井正彦，濱口毅，西田直樹，坂部俊樹，草刈圭一朗,
    例外処理を持つ関数型プログラムの停止性証明法,
    第12回プログラミングおよびプログラミング言語ワークショップ PPL2010, 論文集 p.81 (ポスター・デモ発表), Mar 2010.
  8. 西田直樹, 中林直生, 酒井正彦, 草刈圭一朗, 坂部俊樹,
    制約付き等式の定理自動証明器の試作,
    日本ソフトウェア科学会第26回大会講演論文集, 5P-4 (ポスター・デモ発表), Sep 2009.
  9. KOJIMA Yoshiharu, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki,
    Context-Sensitive Innermost Reachability is Decidable for Linear Right-Shallow Term Rewriting Systems,
    In the 72nd Workshop on IPSJ Special Interest Group on Programming, documents distributed, pp.1-11, Jan 2009.
  10. KUSAKARI Keiichirou,
    Characterizing, Proving and Disproving Inductive Theorems in Higher-Order Rewriting,
    The 24th Workshop on Term Rewriting Systems, Simane Univ., Apr 2004.
  11. K.Kusakari,
    Argument Filtering Methods in Simply-Typed Term Rewriting Systems,
    The 23rd Workshop on Term Rewriting Systems, Nagoya Univ., Sep 2003.
  12. K.Kusakari and M.Sakai,
    On Proving Termination of HRSs w.r.t. call-by-value reduction,
    The 21st Workshop on Term Rewriting Systems, JAIST, Nov 2002.
  13. K.Kusakari,
    Path Orders in Simply-Typed Term Rewriting Systems,
    The 20th Workshop on Term Rewriting Systems, Tsukuba Univ., Mar 2002.
  14. K.Kusakari,
    Lexicographic Path Orders in Simply-Typed TRSs,
    The 18th Workshop on Term Rewriting Systems, Tohoku Univ., Sendai, Mar 2001.
  15. K.Kusakari,
    RPO, DP and AF-method on TRS with Higher-Order Variables,
    The 17th Workshop on Term Rewriting Systems,
    Osaka Life Electronics Research Center, Electrotechnical Laboratory, Amagasaki, Nov 2000.
  16. K.Kusakari, Y.Toyama,
    On Proving Termination of Higher-Order Term Rewriting Systems,
    The 16th Workshop on Term Rewriting Systems, Gunma Univ., Kiryu, Mar 2000.
  17. K.Kusakari,
    Argument Filtering Transformation and its Extension to AC-TRSs,
    The 15th Workshop on Term Rewriting Systems, Kyusyu Univ., Yufuin, Nov 1999.
  18. K.Kusakari, Y.Toyama,
    The Hierarchy of Dependency Pairs,
    The 14th Workshop on Term Rewriting Systems, Nara Institute of Science and Technology, Nara, Mar 1999.
  19. K.Kusakari, Y.Toyama,
    On Proving AC-Termination by Dependency Pairs,
    The 12nd Workshop on Term Rewriting Systems, Nagoya Univ., Nov 1997.
  20. K.Kusakari,
    On the Church-Rosser Property of Left-linear TRS's with One Non-linear Rule,
    The Workshop on Term Rewriting Systems, JAIST, Mar 1997.
  21. K.Kusakari,
    A Transformation Method Preserving Unique Normal Form Property,
    The 10th Workshop on Term Rewriting Systems, NTT Communication Science Labs., Oct 1996.
[Top Page]