Other publications

Selected Publications


  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), Blasilia, Blazil,
    Lecture Notes in Computer Science, to appear.

  2. 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, to appear.

  3. Kentaro Shimanuki, Takahito Aoto and Yoshihito Toyama,
    Decision method of reachability based on rewrite rule overlapping (in Japanese),
    Computer Software, Vol.33, No.3, pp.93-107, 2016.

  4. 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.

  5. 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.

  6. 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.

  7. Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
    Correctness of context-moving transformations for term rewriting systems,
    In Proceedings of 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.

  8. 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.

  9. Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
    Automated inductive theorem proving using transformations of term rewriting systems (in Japanese),
    Computer Software, Vol.32, No.1, pp.179-193, 2015.

  10. Tatsunari Nakazima, Takahito Aoto and Yoshihito Toyama,
    Decidability of inductive theorems based on rewriting induction (in Japanese),
    Computer Software, Vol.31, No.3, pp.294-306, 2014.

  11. 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.

  12. Shota Takahashi, Takahito Aoto and Yoshihito Toyama,
    Innermost reachability of bottom-up innermost term rewriting systems (in Japanese),
    Computer Software, Vol.31, No.1, pp.75-89, 2014.

  13. Tsubasa Suzuki, Takahito Aoto and Yoshihito Toyama,
    Confluence proofs of term rewriting systems based on persistency (in Japanese),
    Computer Software, Vol.30, No.3, pp.148-162, 2013.

  14. Masaki Matoba, Takahito Aoto and Yoshihito Toyama,
    Commutativity of term rewriting systems based on one side decreasing diagrams (in Japanese),
    Computer Software, Vol.30, No.1, pp.187-202, 2013.

  15. 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.

  16. Kouki Isobe, Takahito Aoto, Yoshihito Toyama,
    A Path-Order of Term Rewriting Systems for Polynomial-Size Normal Forms (in Japanese),
    Computer Software, Vol.29, No.1, pp.176-190, 2012.

  17. 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.

  18. 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.

  19. Takahito Aoto, Junichi Yoshida, Yoshihito Toyama,
    Proving Confluence of Term Rewriting Systems Automatically,
    In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009),
    Lecture Notes in Computer Science Vol.5595, pp.93-102, 2009.

  20. Junichi Yoshida, Takahito Aoto, Yoshihito Toyama,
    Automating Confluence Check of Term Rewriting Systems (in Japanese),
    JSSST Computer Software Vol.26, No.2, pp,76-92, 2009.

  21. Satoshi Shimazu, Takahito Aoto, Yoshihito Toyama,
    Automated Lemma Generation for Rewriting Induction with Disproof (in Japanese),
    JSSST Computer Software Vol.26, No.2, pp.41-55, 2009.

  22. 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.

  23. 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),
    Lecture Notes in Computer Science, Vol.5117, pp.381-391, 2008.

  24. 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.

  25. Junichi Yoshida, Takahito Aoto and Yoshihito Toyama,
    Automating confluence check of term rewriting systems (in Japanese),
    Forum on Information Technology 2007 (FIT 2007), Information Technology Letters, Vol.6, pp.31-34, 2007.

  26. 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.

  27. Keiichirou Kusakari, Masaki Nakamura and Yoshihito Toyama,
    Elimination Transformations for Associative-Commutative Rewriting Systems,
    Journal of Automated Reasoning, Vol.37, No.3, pp.205-229, 2006.

  28. 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.

  29. Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
    Introducing sequence variables in program transformation based on templates (in Japanese),
    Forum on Information Technology 2005 (FIT 2005), Information Technology Letters, Vol.4, pp.5-8, 2005.

  30. 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), pp.59-69, 2005.

  31. Yoshihito Toyama,
    Confluent Term Rewriting Systems (Invited Talk),
    In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005),
    Lecture Notes in Computer Science, Vol.3467, p.1, 2005. [Abstract] [Slide]

  32. Yoshihito 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),
    Lecture Notes in Computer Science, Vol.3091, pp.40-54, 2004.

  33. Takahito Aoto, Toshiyuki Yamada and Yoshihito Toyama,
    Inductive theorems for higher-order rewriting,
    In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004),
    Lecture Notes in Computer Science, Vol.3091, pp.269-284, 2004.

  34. Takahito Aoto, Toshiyuki Yamada and Yoshihito Toyama,
    Proving inductive theorems of higher-order functional programs (in Japanese),
    Forum on Information Technology 2003 (FIT 2003), Information Technology Letters, Vol.2, pp.21-22, 2003.

  35. Takashi Nagaya and Yoshihito Toyama,
    Decidability for left-linear growing term rewriting systems,
    Information and Computation Vol.178, pp.499-514, 2002.

  36. Yoshihito Toyama,
    Equational Proofs by Completion: A tutorial (in Japanese),
    Journal of Japanese Society for Artificial Intelligence, Vol.16, No.5, pp.668-674, 2001.

  37. Keiichirou Kusakari and Yoshihito Toyama,
    On Proving AC-Termination by AC-Dependency Pairs,
    IEICE Transactions on Information and Systems, Vol.E84-D, No.5, pp.604-612, 2001.

  38. Yoshihito Toyama and Michio Oyamaguchi,
    Church-Rosser Property and Unique Normal Form Property of Non-Duplicating Term Rewriting Systems,
    IEICE Transactions on Information and Systems, Vol.E84-D, No.4, pp.439-447, 2001.

  39. Yoshihito Toyama,
    New Challenges for Computational Models (Position Paper),
    In Proceedings of IFIP International Conference on Theoretical Computer Science,
    Lecture Notes in Computer Science, Vol.1872, pp.612-613, 2000.

  40. Hirotaka Koike and Yoshihito Toyama,
    Comparison between Inductionless Induction and Rewriting Induction (in Japanese),
    JSSST Computer Software Vol.17, No.6, pp.1-12, 2000.

  41. Keiichirou Kusakari and Yoshihito Toyama,
    On Proving AC-Termination by Argument Filtering Method,
    IPSJ Transactions on Programming, Vol.41, No.SIG 4 (PRO 7), pp.65-78, 2000.

  42. Masaki Nakamura, Keiichirou Kusakari and Yoshihito Toyama,
    On Proving Termination by General Dummy Elimination (in Japanese),
    IEICE Transactions on Information and Systems, Vol. J82-D-I, No.10, pp.1225-1231, 1999.

  43. Keiichirou Kusakari, Masaki Nakamura and Yoshihito Toyama,
    Argument Filtering Transformation,
    In Proceedings of International Conference on Principles and Practice of Declarative Programming (PPDP 99),
    Lecture Notes in Computer Science, Vol.1702, pp.47-61, 1999.

  44. Munehiro Iwami and Yoshihito Toyama,
    Simplification ordering for higher-order rewrite systems,
    IPSJ Transactions on Programming, Vol.40, No.SIG 4 (PRO 3), pp.1-10, 1999.

  45. Munehiro Iwami, Masahiko Sakai and Yoshihito Toyama,
    An improved recursive decomposition ordering for higher-order rewrite systems,
    IEICE Transactions on Information and Systems, Vol.E81-D, No.9, pp.988-996, 1998.

  46. Masahiko Sakai and Yoshihito Toyama,
    Semantics and strong sequentiality of priority term rewriting systems,
    Theoretical Computer Science, Vol.208, pp.87-110, 1998.

  47. Takashi Nagaya, Masahiko Sakai and Yoshihito Toyama,
    Index reduction of overlapping strongly sequential systems,
    IEICE Transactions on Information and Systems, Vol.E-81D, No.5, pp.419-426, 1998.

  48. Takahito Aoto and Yoshihito Toyama,
    Termination transformation by tree lifiting ordering,
    In Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA 98),
    Lecture Notes in Computer Science, Vol.1379, pp.256-270, 1998.

  49. Takahito Aoto and Yoshihito Toyama,
    On composable properties of term rewriting systems,
    In Proceedings of the 6th International Conference on Algebraic and Logic Programming (ALP 97),
    Lecture Notes in Computer Science, Vol.1298, pp.114-128, 1997.

  50. Takahito Aoto and Yoshihito Toyama,
    Persistency of confluence,
    Journal of Universal Computer Science, Vol.3, No.11, pp.1134-1147, 1997.

  51. Yositaka Takahashi, Masahiko Sakai and Yoshihito Toyama,
    On the confluence property of conditional term rewriting systems (in Japanese),
    IEICE Transactions, Vol.J79-D-I, No.11, pp.897-902, 1996.

  52. Masahiko Sakai and Yoshihito Toyama,
    Semantics and strong sequentiality of priority term rewriting systems,
    In Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA 96),
    Lecture Notes in Computer Science, Vol.1103, pp.377-391, 1996.

  53. Yoshikatsu Ohta, Michio Oyamaguchi and Yoshihito Toyama,
    On the confluence property of simple-right-linear term rewriting systems (in Japanese),
    IEICE Transactions, Vol.J78-D-I, No.3, pp.263-268, 1995.

  54. Yoshihito Toyama, Jan Willem Klop and Henk Pieter Barendregt,
    Termination for direct sums of left-linear complete term rewriting systems,
    Journal of the Association for Computer Machinery, Vol.42, No.6, pp.1275-1304, 1995.

  55. Jan Willem Klop, Aart Middeldorp, Yoshihito Toyama and Roel de Vrijer,
    Modularity of confluence: A simplified proof,
    Information Processing Letters, Vol.49, pp.101-109, 1994.

  56. Yoshihito Toyama and Michio Oyamaguchi,
    Church-Rosser property and unique normal formal property of non-duplicating term rewriting systems,
    In Proceedings of the 4th International Conference on Conditional and Typed Rewrite Systems (CTRS 94),
    Lecture Notes in Computer Science, Vol.968, pp.316-331, 1994.

  57. Aart Middeldorp and Yoshihito Toyama,
    Completeness of combination of constructor systems,
    Journal of Symbolic Computation, Vol.15, pp.331-348,1993.

  58. Yoshihito Toyama, Sjaak Smetsers, Marko van Eeklen, Rinus Plasmeijer,
    The functional strategy and transitive term rewriting systems,
    in: M.R. Sleep, etc., eds., Term Graph Rewriting, pp.61-75, (Wiley, 1993).

  59. Yoshihito Toyama,
    Strong sequentiality of left-linear overlapping term rewriting systems,
    In Proceedings of the 7th IEEE Symposium on Logic in Computer Science (LICS 92), pp.274-284, 1992.

  60. Yoshihito Toyama,
    How to prove equivalence of term rewriting systems without induction,
    Theoretical Computer Science, Vol.90, pp.369-390, 1991.

  61. Aart Middeldorp and Yoshihito Toyama,
    Completeness of combinations of constructor systems,
    In Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA 91),
    Lecture Notes in Computer Science, Vol.488, pp.188-198, 1991.

  62. Yoshihito Toyama,
    Term rewriting systems and the Church-Rosser property,
    Doctoral Thesis, Tohoku University, 1990.

  63. Yoshihito Toyama,
    Membership conditional term rewriting systems,
    IEICE Transactions, Vol.E72, No.11, pp.1224-1229, 1989.

  64. Yoshihito Toyama,
    Fast Knuth-Bendix completion with a term rewriting system compiler,
    Information Processing Letters, Vol.32, pp.325-328, 1989.

  65. Yoshihito Toyama, Jan Willem Klop and Henk Pieter Barendregt,
    Termination for the direct sum of left-linear term rewriting systems: Preliminary draft,
    In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications (RTA 89),
    Lecture Notes in Computer Science, Vol.355, pp.477-491, 1989.

  66. Yoshihito Toyama,
    Confluent term rewriting systems with membership conditions,
    In Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems (CTRS 88),
    Lecture Notes in Computer Science, Vol.308, pp.228-241, 1988.

  67. Yoshihito Toyama,
    Commutativity of term rewriting systems,
    in: K. Fuchi and L. Kott, eds., Programming of Future Generation Computer II, pp.393-407, (North-Holland, 1988).

  68. Yoshihito Toyama,
    Counterexamples to termination for the direct sum of term rewriting systems,
    Information Processing Letters, Vol.25, pp.141-143, 1987.

  69. Yoshihito Toyama,
    On the Church-Rosser property for the direct sum of term rewriting systems,
    Journal of the Association for Computer Machinery, Vol.34, No.1, pp.128-143, 1987.

  70. Tetsuo Ida, Akira Aiba and Yoshihito Toyama,
    T: A simple reduction language based on combinatory term rewriting,
    in: K. Fuchi and M. Nivat, eds., Programming of Future Generation Computer I, pp.217-236, (North-Holland, 1986).

  71. Yoshihito Toyama,
    How to prove equivalence of term rewriting systems without induction,
    In Proceedings of the 8th International Conference on Automated Deduction (CADE 86),
    Lecture Notes in Computer Science, Vol.230, pp.118-127, 1986.

  72. Toshiharu Sugawara and Yoshihito Toyama,
    Theory of inductive inference: A tutorial (in Japanese),
    Journal of the Society of Instrument and Control Engineers, Vol.25, No.9, pp.781-786, 1986.

  73. Yoshihito Toyama,
    On equivalence transformations for term rewriting systems,
    In Proceedings of RIMS Symposia on Software Science and Engineering II,
    Lecture Notes in Computer Science, Vol.220, pp.44-61, 1985.

  74. Yoshihito Toyama,
    A comment on call by need (in Japanese),
    Journal of Information Processing Society of Japan, Vol.25, No.3, pp.249-251, 1984.

  75. Yoshihito Toyama,
    On commutativity of term rewriting systems (in Japanese),
    IEICE Transactions, Vol.J66-D, No.12, pp.1370-1375, 1983.

  76. Kokichi Futatsugi and Yoshihito Toyama,
    Term rewriting systems and their applications: A survey (in Japanese),
    Journal of Information Processing Society of Japan, Vol.24, No.2, pp.133-146, 1983.

  77. Yoshihito Toyama and Masayuki Kimura,
    On Learning automata in non-stationary random environments,
    In Proceedings of IEEE Symposium on Cybernetics and Society, pp.1482-1486, 1978.

  78. Yoshihito Toyama and Masayuki Kimura,
    On Learning automata in non-stationary random environments (in Japanese),
    IEICE Transactions, Vol.J60-D, No.12, pp.1085-1092, 1977.


Other publications   Toyama's page   Toyama-Aoto laboratory