国際会議や学術雑誌での発表論文

1. Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
   Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems,
   In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Brasilia, Brazil,
   Lecture Notes in Computer Science, Vol.10483, pp.115-131, 2017.
2. Kentaro Kikuchi,
   Confluence by Strong Commutation with Disjoint Parallel Reduction,
   In Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), Oxford, UK, pp.9:1-9:10, 2017.
3. Takahito Aoto, Yoshihito Toyama and Yuta Kimura,
   Improving rewriting induction approach for proving ground confluence,
   In Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Oxford, UK,
   Leibniz International Proceedings in Informatics, Vol.84, pp.7:1-7:18, 2017.
4. 島貫健太郎, 青戸等人, 外山 芳人,
   書き換え規則の重なりに基づく到達可能性判定法,
   コンピュータソフトウェア, Vol.33, No.3, pp.93-107, 2016.
   
5. Takahito Aoto and Kentaro Kikuchi,
   Nominal confluence tool,
   In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal,
   Lecture Notes in Computer Science, Vol.9706, pp.173-182, 2016.
6. Takahito Aoto and Kentaro Kikuchi,
   A rule-based procedure for equivariant nominal unification,
   In Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016), Porto, Portugal, 2016.
   
7. Vincent van Oostrom and Yoshihito Toyama,
   Normalisation by random descent,
   In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Porto, Portugal,
   Leibniz International Proceedings in Informatics, Vol.52, pp.32:1-32:18, 2016.
8. Takahito Aoto and Yoshihito Toyama,
   Ground confluence prover based on rewriting induction,
   In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Porto, Portugal,
   Leibniz International Proceedings in Informatics, Vol.52, pp.33:1-33:12, 2016.
9. Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
   Critical pair analysis in nominal rewriting,
   In Proceedings of the 7th International Symposium on Symbolic Computation in Software Science (SCSS 2016), Tokyo, Japan,
   EPiC Series in Computing, Vol.39, pp.156-168, 2016.
10. Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
    Correctness of context-moving transformations for term rewriting systems,
    In Proceedings of the 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015), Siena, Italy,
    Lecture Notes in Computer Science, Vol.9527, pp.331-345, 2015.
11. Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
    Confluence of orthogonal nominal rewriting systems revisited,
    In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Warsaw, Poland,
    Leibniz International Proceedings in Informatics, Vol.36, pp.301-317, 2015.
12. 佐藤洸一, 菊池健太郎, 青戸等人, 外山 芳人,
    項書き換えシステムの変換を利用した帰納的定理自動証明,
    コンピュータソフトウェア, Vol.32, No.1, pp.179-193, 2015.
    
13. Kentaro Kikuchi and Takafumi Sakurai,
    A translation of intersection and union types for the λμ-calculus,
    In Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), Singapore,
    Lecture Notes in Computer Science, Vol.8858, pp.120-139, 2014.
14. Takahito Aoto and Sorin Stratulat,
    Decision procedures for proving inductive theorems without induction,
    In Proceedings of 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014), Canterbury, UK, September 2014, pp.237-248, ACM Press.
15. 中嶋辰成, 青戸等人, 外山芳人,
    書き換え帰納法に基づく帰納的定理の決定可能性,
    コンピュータソフトウェア, Vol.31, No.3, pp.294-306, 2014.
    
16. Takahito Aoto, Yoshihito Toyama and Kazumasa Uchida,
    Proving confluence of term rewriting systems via persistency and decreasing diagrams,
    In Proceedings of Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Vienna, Austria, LNCS 8560, pp.46-60, 2014.
17. Kentaro Kikuchi,
    Uniform proofs of normalisation and approximation for intersection types,
    In Proceedings of the 7th Workshop on Intersection Types and Related Systems (ITRS 2014), Vienna, Austria, 2014.
18. Kentaro Kikuchi and Takafumi Sakurai,
    A translation of intersection and union types for the λμ-calculus,
    In Proceedings of the 5th International Workshop on Classical Logic and Computation (CL&C 2014), Vienna, Austria, 2014.
19. 高橋翔大, 青戸等人, 外山芳人,
    ボトムアップ最内項書き換えシステムの最内到達可能性,
    コンピュータソフトウェア, Vol.31, No.1, pp.75-89, 2014.
    
20. Takahito Aoto,
    Disproving confluence of term rewriting systems by interpretation and ordering,
    In Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Nancy, France, LNAI 8152, pp.311-326, 2013.
21. Kentaro Kikuchi,
    Proving strong normalisation via non-deterministic translations into Klop's extended λ-calculus,
    In Proceedings of the 22nd Annual Conference of the European Association for Computer Science Logic (CSL 2013), LIPIcs 23, pp.395-414, 2013.
22. 鈴木翼, 青戸等人, 外山芳人,
    永続性にもとづく項書き換えシステムの合流性証明,
    コンピュータソフトウェア, Vol.30, No.3, pp.148-162, 2013.
    

23. Takahito Aoto,
    Disproving confluence of term rewriting systems by interpretation and ordering (extended abstract),
    In Proceedings of the 2nd International Workshop on Confluence (IWC 2013), Eindhoven, The Netherlands, pp.5-9, 2013
    

24. Takahito Aoto and Munehiro Iwami,
    Termination of rule-based calculi for uniform semi-unification,
    In Proceedings of the 7th International Conference on Language and Automata Theory and Applications (LATA 2013), Bilbao, Spain, LNCS 7810, pp.56-67, 2013.
25. 的場正樹, 青戸等人, 外山芳人,
    片側減少ダイアグラム法による項書き換えシステムの可換性証明法,
    コンピュータソフトウェア, Vol.30, No.1, pp.187-202, 2013.
    

26. Takahito Aoto and Jeroen Ketema,
    Rational term rewriting revisited: decidability and confluence,
    In Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012), Bremen, Germany, LNCS 7562, pp.172-186, 2012.

27. Yuki Chiba and Takahito Aoto,
    Transformations by templates for simply-typed term rewriting,
    In Proceedings of the 6th International Workshop on Higher-Order Rewriting (HOR 2012), Nagoya, Japan, pp.3-8, 2012.

28. Takahito Aoto and Yoshihito Toyama,
    A reduction-preserving completion for proving confluence of non-terminating term rewriting systems,
    Logical Methods in Computer Science, Vol.8, No.1:31, pp.1-29, 2012.

29. 岩見宗弘, 青戸等人,
    無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証,
    コンピュータソフトウェア, Vol.29, No.1, pp.211-239, 2012.
    

30. 磯部耕己, 青戸等人, 外山芳人,
    多項式サイズ正規形を保証する項書き換えシステムの経路順序, コンピュータソフトウェア, Vol.29, No.1, pp.176-190, 2012.
    

31. Takahito Aoto, Toshiyuki Yamada and Yuki Chiba,
    Natural inductive theorems for higher-order rewriting,
    In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Novi Sad, Serbia,
    Leibniz International Proceedings in Informatics, Vol.10,pp.107-121, 2011.

32. Takahito Aoto and Yoshihito Toyama,
    Reduction-preserving completion for proving confluence of non-terminating term rewriting systems,
    In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Novi Sad, Serbia,
    Leibniz International Proceedings in Informatics, Vol.10, pp.91-106, 2011.

33. Takahito Aoto,
    Automated confluence proof by decreasing diagrams based on rule-labelling,
    In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Edingburgh, UK,
    Leibniz International Proceedings in Informatics, Vol.6, pp.7-16, 2010.

34. Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
    Program transformation templates for tupling based on term rewriting,
    IEICE Transactions on Information and Systems, Vol.E93-D, No.5, pp.963-973, 2010.
35. Takahito Aoto and Toshiyuki Yamada,
    Argument filterings and usable rules for simply typed dependency pairs,
    In Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009), Trento, Italy, LNAI 5749, pp.117-132, 2009.
36. Takahito Aoto, Junichi Yoshida and Yoshihito Toyama,
    Proving confluence of term rewriting systems automatically,
    In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Brasília, Brazil, LNCS 5595, pp.93-102, 2009.
37. 吉田順一, 青戸等人, 外山 芳人,
    項書き換えシステムの合流性自動判定,
    コンピュータソフトウェア, Vol.26, No.2, pp.76-92, 2009.
38. 嶌津聡志, 青戸等人, 外山 芳人,
    反証機能付き書き換え帰納法のための補題自動生成法,
    コンピュータソフトウェア, Vol.26, No.2, pp.41-55, 2009.
39. Takahito Aoto,
    Sound lemma generation for proving inductive validity of equations,
    In Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), Bangalore, India, Dagstuhl Seminar Proceedings, Vol.08004, pp.13-24, 2008.
    

40. Jean-Pierre Jouannaud and Yoshihito Toyama,
    Modular Church-Rosser Modulo: The Complete Picture,
    International Journal of Software and Informatics, Vol.2, No.1, pp.61-75, 2008.
41. Yoshihito Toyama,
    Termination proof of S-expression rewriting systems with recursive path relations,
    In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Hagenberg, Austria, LNCS 5117, pp.381-391, 2008.
42. Jeroen Ketema,
    On normalisation of infinitary combinatory reduction systems,
    In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Hagenberg, Austria, LNCS 5117, pp.172-186, 2008.
43. Takahito Aoto,
    Designing a rewriting induction prover with an increased capability of non-orientable theorems,
    In Proceedings of Austrian-Japanese Workshop on Symbolic Computation in Software Science (SCSS 2008), Hagenberg, Austria, pp.1-15, 2008.
44. Kentaro Kikuchi,
    Call-by-name reduction and cut-elimination in classical logic,
    Annals of Pure and Applied Logic, Vol.153, No.1-3, pp.38-65, 2008.
45. Kentaro Kikuchi and Stéphane Lengrand,
    Strong normalisation of cut-elimination that simulates β-reduction,
    In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2008), LNCS 4962, pp.380-394, 2008.
    
46. Takahito Aoto,
    Soundness of rewriting induction based on an abstract principle,
    IPSJ Transactions on Programming, Vol.49, No.SIG 1 (PRO 35), pp.28-38, 2008.
47. Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
    Automatic construction of program transformation templates,
    IPSJ Transactions on Programming, Vol.49, No.SIG 1 (PRO 35), pp.14-27, 2008.
48. 吉田順一, 青戸等人, 外山芳人,
    項書き換えシステムの合流性自動判定.
    第6回情報科学技術フォーラム(FIT2007)講演論文集, 情報技術レターズ, Vol.6, pp.31-34, 2007.
49. Ryo Ishigaki and Kentaro Kikuchi,
    Tree-Sequent Methods for Subintuitionistic Predicate Logics,
    In Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007), LNAI 4548, pp.149-164, 2007.
50. Kentaro Kikuchi,
    Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi,
    In Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), LNCS 4533, pp.257-272, 2007.
51. Joerg Endrullis and Jeroen Ketema,
    Root Stabilisation Using Dependency Pairs,
    In Proceedings of the 9th International Workshop on Termination (WST 2007), pp.17-21, 2007.
52. Takahito Aoto and Toshiyuki Yamada,
    Argument filterings and usable rules for simply typed dependency pairs (extended abstract),
    In Proceedings of the 4th International Workshop on Higher-Order Rewriting (HOR 2007), Paris, France, pp.21-27， 2007．
53. Kentaro Kikuchi,
    Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus,
    In Proceedings of the 3rd Conference on Computability in Europe (CiE 2007), LNCS 4497, pp.398-407, 2007.
54. Ryo Ishigaki and Kentaro Kikuchi,
    A Tree-Sequent Calculus for a Natural Predicate Extension of Visser's Propositional Logic,
    Logic Journal of the Interest Group in Pure and Applied Logics, Vol.15, No.2, pp.149-164, 2007.
55. Keiichirou Kusakari, and Yuki Chiba,
    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.
56. Kentaro Kikuchi,
    On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus,
    In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2006), LNAI 4246, pp.120-134, 2006.
57. 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.
58. Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
    Program Transformation by Templates: A Rewriting Framework,
    IPSJ Transactions on Programming, Vol.47, No.SIG 16 (PRO 31), pp.52-65, 2006.
59. Yuki Chiba and Takahito Aoto,
    RAPT: A Program Transformation System based on Term Rewriting,
    In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006),
    Seattle, WA, USA, Lecture Notes in Computer Science, Vol.4098, Springer-Verlag, pp.267-276, 2006.
60. Takahito Aoto,
    Dealing with Non-orientable Equations in Rewriting Induction,
    In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006),
    Seattle, WA, USA, Lecture Notes in Computer Science, Vol.4098, Springer-Verlag, pp.242-256, 2006.
61. Kentaro Kikuchi,
    Call-by-Name Reduction and Cut-Elimination in Classical Logic,
    In Proceedings of the 1st International Workshop on Classical Logic and Computation (CL&C 2006), 2006.
62. Yoshihito Toyama,
    Reduction strategies for left-linear term rewriting systems,
    In Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday,
    Lecture Notes in Computer Science, Vol.3838, pp.198-223, 2005.
63. Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
    Introducing Sequence Variables in Program Transformation based on Templates,
    In Proceedings of the Forum on Information Technology 2005 (FIT2005), Information Technology Letters, Vol.4, pp.5-8, 2005 (in japanese).
64. Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
    Program Transformation by Templates based on Term Rewriting,
    In Proceedings of the 7th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2005), ACM Press, pp.59-69, 2005.
65. Yoshihito Toyama,
    Confluent Term Rewriting Systems, Invited Talk,
    In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005), Nara, Japan,
    Lecture Notes in Computer Science, Vol.3467, Springer-Verlag, p.1, 2005. [Slide]
66. Takahito Aoto and Toshiyuki Yamada,
    Dependency Pairs for Simply Typed Term Rewriting,
    In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005), Nara, Japan,
    Lecture Notes in Computer Science, Vol.3467, Springer-Verlag, pp.120-134, 2005.
67. Y.Toyama,
    Termination of S-expression rewriting systems: Lexicographic path ordering for higher-order terms,
    In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), Aachen, Germany,
    Lecture Notes in Computer Science, Vol.3091, Springer-Verlag, pp.40-54, 2004.
68. T.Aoto, T.Yamada and Y.Toyama,
    Inductive theorems for higher-order rewriting,
    In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), Aachen, Germany,
    Lecture Notes in Computer Science, Vol.3091, Springer-Verlag, pp.269-284, 2004.
69. T.Aoto and T.Yamada,
    Termination of simply-typed applicative term rewriting systems,
    In Proceedings of the 2nd International Workshop on Higher-Order Rewriting (HOR 2004), Aachen, Germany,
    Technical Report 2004-03, Department of Computer Science, RWTH Aachen, pp.61-65, 2004.
70. T.Aoto, T.Yamada and Y.Toyama,
    Proving inductive theorems of higher-order functional programs,
    In Proceedings of the Forum on Information Technology 2003 (FIT2003),
    Information Technology Letters, Vol.2, pp.21-22, 2003 (in japanese).
71. T.Aoto and T.Yamada,
    Termination of simply typed term rewriting systems by translation and labelling,
    In Proceedings of the 14th International Conference on Rewriting Techniques and Applications, Valencia, Spain,
    Lecture Notes in Computer Science, Vol.2706, Springer-Verlag pp.380-394, 2003.
72. T.Aoto and T.Yamada,
    Proving Termination of Simply Typed Term Rewriting Systems Automatically,
    IPSJ Trans. Programming, Vol. 44, No.SIG 4 (PRO17), pp.67-77, 2003 (in Japanese).
73. T.Nagaya and Y.Toyama,
    Decidability for left-linear growing term rewriting systems,
    Information and Computation Vol.178, pp.499-514, 2002.
74. 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), Copenhagen, Denmark, July 21, p.25, 2002.
75. 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), Sendai, Japan, October 25-27, pp.176-187, 2001.
76. Y.Toyama,
    Equational Proofs by Completion,
    Journal of Japanese Society for Artificial Intelligence, Vol.16, No.5, pp.668-674, 2001 (Survey Paper; in Japanese).
77. 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.
78. 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. [draft]
79. Y.Toyama and M.Oyamaguchi,
    Conditional Linearization of Non-Duplicating Term Rewriting Systems,
    IEICE Transactions on Information and Systems, Vol.E84-D, No.4, pp.439-447, 2001.
80. Taro Suzuki and Aart Middeldorp,
    A Complete Selection Function for Lazy Conditional Narrowing,
    FLOPS'01, Proceedings of the 5th International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science 2024, pp.201-215, 2001.
81. Y.Toyama,
    New Challenges for Computational Models,
    Proc. of Int. Conf. IFIP Theoretical Computer Science, Lecture Notes in Computer Science 1872, pp.612-613, 2000 (Panel Discussion).
82. H.Koike, Y.Toyama,
    Comparison between Inductionless Induction and Rewriting Induction,
    JSSST Computer Software Vol.17, No.6, pp.1-12, 2000 (in Japanese).
83. 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.

北陸先端科学技術大学院大学 外山・酒井研 (1993.4-1997.3)／外山研 (1997.4-2000.3)における発表論文は国際会議や学術雑誌における発表論文(JAIST)へ．

webmaster