Publications of Toyama-Aoto Laboratory

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.

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

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

  13. 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, June 2012, pp.3-8.

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

  15. Munehiro Iwami and Takahito Aoto,
    Disproving strong head normalization and general productivity automatically in infinitary term rewriting systems (in japanese),
    Computer Software, Vol.29, No.1, pp.211-239, 2012.

  16. Kouki Isobe, Takahito Aoto and Yoshihito Toyama,
    A path ordering for term rewriting systems with polynomial size normal forms (in japanese),
    Computer Software, Vol.29, No.1, pp.176-190, 2012.

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

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

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

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

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

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

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

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

  25. 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, LIPIcs, Vol.2, pp.13-24, 2008.

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

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

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

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

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

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

  32. Yuki Chiba,
    A Term Rewriting Approach to Program Transformation by Templates,
    Ph.D. Thesis, Tohoku University, 2008.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  50. 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).

  51. 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), ACP Press, pp.59-69, 2005.

  52. 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]

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

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

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

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

  57. Takahito Aoto, Toshiyuki Yamada and Yoshihito 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).

  58. Takahito Aoto and Toshiyuki 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.

  59. 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).

  60. T.Nagaya and Y.Toyama,
    Decidability for left-linear growing term rewriting systems,
    Information and Computation Vol.178, (2002) 499-514.

  61. 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).

  62. 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).

  63. 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).

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

  65. 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]

  66. Y.Toyama and M.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.

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

  68. 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).

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

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


Publications of Toyama Laboratory in JAIST (1997.4-2000.3)

  1. K.Kusakari,
    Termination, AC-Termination and Dependency Pairs of Term Rewriting Systems,
    Ph.D. Thesis, JAIST, 2000.

  2. Mircea Marin, Tetsuo Ida, and Taro Suzuki,
    On Reducing the Search Space of Higher-Order Lazy Narrowing,
    FLOPS'99, Proceedings of the 4th International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science 1722, pp.319-334, 1999.

  3. 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).

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

  5. Munehiro Iwami,
    Termination of Higher-Order Rewrite Systems,
    Ph.D. Thesis, JAIST, 1999.

  6. Takashi Nagaya,
    Reduction Strategies for Term Rewriting Systems,
    Ph.D. Thesis, JAIST, 1999.

  7. Mohamed Hamada, Aart Middeldorp and Taro Suzuki,
    Completeness Results for a Lazy Conditional Narrowing Calculus,
    DMTCS'99, Proceedings of Discrete Mathematics and Theoretical Computer Science, 1999.

  8. M. Iwami, Y. Toyama,
    Simplification ordering for higher-order rewrite systems,
    IPSJ Trans. on Programming, Vol.40, No.SIG 4 (PRO 3), pp.1-10, 1999.

  9. M. Iwami, M. Sakai, Y. Toyama,
    An improved recursive decomposition ordering for higher-order rewrite systems,
    Trans. of IEICE, Vol. E81-D, No. 9, pp. 988-996, 1998.

  10. Masahiko Sakai, Yoshihito Toyama,
    Semantics and Strong Sequentiality of Priority Term Rewriting Systems,
    Theoretical Computer Science, Vol.208, pp.87-110(1998).

  11. T. Aoto, Y. Toyama,
    Termination transformation by tree lifiting ordering,
    in Proc. of the 9th International Conference on Rewrite Techniques and Applications (RTA'98), LNCS 1379, pp. 256-270, 1998.

  12. T. Aoto, Y. Toyama,
    Persistency of confluence,
    Journal of Universal Computer Science, Vol. 3, No. 11, pp. 1134-1147, 1997.

  13. T. Aoto, Y. Toyama,
    On composable properties of term rewriting systems,
    in Proc. of the 6th International Joint Conference, ALP'97 - HOA'97, LNCS Vol. 1298, pp. 114-128, 1997.


Publications of Toyama and Sakai Laboratory in JAIST (1993.4-1997.3)

  1. M. Sakai, Y. Toyama,
    Semantics and strong sequentiality of priority term rewriting systems,
    in Proc. of the 7th International Conference on Rewrite Techniques and Applications (RTA'96), LNCS Vol. 1103, pp. 377-391, 1996.

  2. Y. Takahashi, M. Sakai, Y. Toyama,
    On the confluence property of conditional term rewriting systems,
    Trans. of IEICE, Vol. J79-D-I, No. 11, pp. 1-6, 1996 (in Japanese).

  3. Y. Ohta, M. Oyamaguchi, Y. Toyama,
    On the confluence property of siple-right-linear TRS's
    Trans. of IEICE, Vol. J78-D-I, No. 3, pp. 263-268, 1995 (in Japanese).

  4. Y. Toyama, J. W. Klop, H. P. 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.

  5. S. Yamamoto, R. Ishikawa, M. Sakai, K. Agusa,
    An implimentation of TRS on shared memory multiprocessorts,
    Trans. of IEICE, Vol. J78-D-I, No. 6, pp. 559-562, 1995 (in Japanese).

  6. Y. Hamaguchi, M. Sakai, S. Yamamoto, K. Agusa,
    Error Description on Algebraic Specification and its Automatic Addition,
    Trans. of IEICE, Vol. J78-D-I, No. 3, pp. 323-330, 1995 (in Japanese).

  7. M. Kawakita, M. Sakai, S. Yamamoto, K. Agusa,
    A model for reuse based on formal specifications,
    Trans. of IPSJ, Vol. 36, No. 5, 1995 (in Japanese).

  8. Y. Ohta, M. Oyamaguchi, Y. Toyama,
    On the confluence property of siple-right-linear TRS's
    Trans. of IEICE, Vol. J78-D-I, No. 3, pp. 263-268, 1995 (in Japanese).

  9. J. W. Klop, A. Middeldorp, Y. Toyama, R. de Vrijer,
    Modularity of confluence: A simplified proof,
    Information Processing Letters, Vol. 49, pp. 101-109, 1994.

  10. Y. Toyama, M. Oyamaguchi
    Church-Rosser property and unique normal formal property of non-duplicating term rewriting systems,
    in Proc. of the 4th International Conference on Conditional and Typed Rewrite Systems (CTRS'94), LNCS Vol. 968, pp. 316-331, 1994.

  11. Y. Toyama, S. Smetsers, M. Eeklen, R. Plasmeijer,
    The functional strategy and transitive term rewriting systems,
    in Term Graph Rewriting (M. R. Sleep, etc., eds., Wiley, 1993), pp. 61-75, 1993.

[Toyama-Aoto Lab.] [ RIEC] [Tohoku University]
Please send any requests and comments to webmaster