Twenty Years Later

  • Jean-Pierre Jouannaud
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


The first RTA conference took place in Dijon, in 1985. This year, 2005, it takes place in Nara. Nara and Dijon share a glorious past but can be considered as being “Sleeping Beauties”, after the title of a book by the Nobel price novelist yasunari Kawabata.

Is RTA sleeping on its glorious past? Back in the late 80s, many of us feared that this would soon be the case, that research in rewrite systems was deepening the gap with everyday’s computer science practice, and that we should develop rewrite-based powerful provers that would make a difference with the state of art and help address real applications such as software verification.

More than ten years later this has not really happened in the way we thought it would. What has happened is that many research areas, such as programming languages, constraint solving, first-order provers, proof assistants, security theory, and verification have all been fertilized by ideas coming from term rewriting. In return, our field has been renewed by new problems and techniques coming from outside our small community.

I am convinced that this will continue, and that new subject areas will join the journey. There are at least two reasons. To quote a celebrated sentence that I have read in many papers: Equations are ubiquitous in computer science. This is the first reason: we all like to use equations for modeling problems. The second is that we have developed extremely powerful, sophisticated tools to reason with equations. Many computer scientists do not know these tools. It is our responsibility to preach for their use by showing all we can do with them.


Pattern Match Theorem Prove Security Protocol Proof Assistant Tree Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aiken, A., Wimmers, E.: Type inclusion constraints and type inference. In: Proc. 7th ACM Conference on Functional programming and Computer Archtecture, Copenhaguen, Denmark, pp. 31–41 (1993)Google Scholar
  2. 2.
    Bachmair, L., Ganzinger, H.: Completion of first-order clause with equality by strict superposition. In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol. 516, Springer, Heidelberg (1991)Google Scholar
  3. 3.
    Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, Springer, Heidelberg (1990)Google Scholar
  4. 4.
    Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Technical Report MPI-I-91-208, Max-Planck- Institut für Informatik, Saarbrücken (September 1991); to appear in Journal of Logic and ComputationGoogle Scholar
  5. 5.
    Bachmair, L., Ganzinger, H.: Non-clausal resolution and superposition with selection and redundancy criteria. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, Springer, Heidelberg (1992)CrossRefGoogle Scholar
  6. 6.
    Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, Springer, Heidelberg (1992)Google Scholar
  7. 7.
    Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Proceedings of the Eigth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Los Alamitos (1993)Google Scholar
  8. 8.
    Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure patern type systems. In: Conference Record of the 30th Symposium on Principles of Programming Languages, New-Orleans, USA, January 2003, ACM, New York (2003)Google Scholar
  9. 9.
    Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science 15(1), 37–92 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Blanqui, F.: Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae (to appear)Google Scholar
  11. 11.
    Blanqui, F., Jouannaud, J.-P., Strub, P.-Y.: A calculus of congruent constructions. Technical report, École Polytechnique (2005) (submitted)Google Scholar
  12. 12.
    Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 30–43. Springer, Heidelberg (1996)Google Scholar
  13. 13.
    Boudet, A., Jouannaud, J.-P., Schmidt-Schauß, M.: Unification in Boolean rings and Abelian groups. Journal of Symbolic Computation 8, 449–477 (1989)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 67–92. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  15. 15.
    Bouhoula, A., Jouannaud, J.-P.: Automata-driven automated induction. In: Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw,Poland, June 1997, pp. 14–25. IEEE Comp. Soc. Press, Los Alamitos (1997)CrossRefGoogle Scholar
  16. 16.
    Burstall, R.M., Goguen, J.A.: The semantics of CLEAR, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, Springer, Heidelberg (1980)Google Scholar
  17. 17.
    Caron, A.-C., Coquidé, J.-L., Dauchet, M.: Encompassment properties and automata with constraints. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 328–342. Springer, Heidelberg (1993)Google Scholar
  18. 18.
    Chrzaszcz, J.: Modules in coq are and will be correct. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 135–150. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Comon, H.: Sequentiality, second-order monadic logic and tree automata. In: Kozen, D. (ed.) Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, CA, June 1995, pp. 508–517. IEEE Comp. Soc. Press, Los Alamitos (1995)CrossRefGoogle Scholar
  20. 20.
    Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation 112(2), 167–216 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76, 95–120 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Dershowitz, N.: Equations as programming language. In: Proceedings of the Fourth Jerusalem Conference on Information Technology, Jerusalem, Israe, May 1984, pp. 114–124. IEEE Computer Society, Los Alamitos (1984)Google Scholar
  23. 23.
    Diaconescu, R., Futatsugi, K.: Cafeobj-report: The language, proof techniques and methodologies for object-oriented algebraic specification. AMAST series in Computing, vol. 6. World Scientific, Singapore (1998)Google Scholar
  24. 24.
    Rusinowitch, M., et al.: The aviss security protocols analysis tool – system description. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 349. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  25. 25.
    Fribourg, L., Peixoto, M.V.: Automates concurrents à contraintes. Technique et Science Informatiques 13(6) (1994)Google Scholar
  26. 26.
    Gilleron, R., Tison, S., Tommasi, M.: Solving systems of set constraints using tree automata. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665, Springer, Heidelberg (1993)Google Scholar
  27. 27.
    Gonthier, G., Lévy, J.-J., Mellies, P.-A.: An abstract standardisation theorem. In: Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, CA (1992)Google Scholar
  28. 28.
    Goubault-Larrecq, J.: Résolution ordonnée avec sélection et classes décidables de la logique du premier ordre (2004), available from the webGoogle Scholar
  29. 29.
    Gregoire, B.: Compilation de termes de preuves. Un mariage entre Coq et OCaml. PhD thesis, École Polytechnique, Palaiseau, France (2003)Google Scholar
  30. 30.
    Hermant, O.: A rewriting abstract machine for coq (2004)Google Scholar
  31. 31.
    Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 54–71. Springer, Heidelberg (1987)Google Scholar
  32. 32.
    Comon, D.L.H., Dauchet, M., Tison, S. (eds.): Tree Automata techniques and Applications, Lille, France (2002),
  33. 33.
    Comon, H., Jürsski, Y.: Higher-order matching and tree automata. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, Springer, Heidelberg (1998)CrossRefGoogle Scholar
  34. 34.
    Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the ACM 27(4), 797–821 (1980)zbMATHCrossRefMathSciNetGoogle Scholar
  35. 35.
    Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, Springer, Heidelberg (1980)Google Scholar
  36. 36.
    Jouannaud, J.-P.: Modular associative commutative confluence. Technical report, École Polytechnique (2005)Google Scholar
  37. 37.
    Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, MIT-Press, Cambridge (1991)Google Scholar
  38. 38.
    Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in equational theories without constructors. In: Logic in Computer Science (June 1986)Google Scholar
  39. 39.
    Jouannaud, J.-P., Rubio, A., van Raamsdonk, F.: Higher-order rewriting with types and arities. Technical report, École Polytechnique (2005) (submitted)Google Scholar
  40. 40.
    Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Française d’Intelligence Artificielle 4(3), 9–52 (1990); Special issue on automatic deductionGoogle Scholar
  41. 41.
    Kirchner, C., Moreau, P.: Non deterministic computations in elan. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol. 1589, pp. 168–183. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  42. 42.
    Lankford, D.S.: Canonical inference. Memo ATP-32, University of Texas at Austin (March 1975)Google Scholar
  43. 43.
    Lugiez, D., Moysset, J.-L.: Complement problems and tree automata in AC-like theories. In: Proc. Symp. on Theoretical Aspects of Computer Science, Würzburg (1993); also available as techincal report CRIN 92-R-175Google Scholar
  44. 44.
    Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science 192(1), 3–29 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  45. 45.
    Meseguer, J.: A logical theory of concurrent objects and its realization in the maude language. In: Agha, G., Wegner, P., Yoneezawa, A. (eds.) Research Directions in Object-Based Concurrency (1992) (to appear)Google Scholar
  46. 46.
    Nakagawa, A.T., Futatsugi, K.: An overview of cafe specification environment. In: Proc. of the 1st IEEE International Conference on Formal Engineering Methods, pp. 170–181. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  47. 47.
    Nieuwenhuis, R.: Basic paramodulation and decidable theories. In: Felty, A. (ed.) Eleventh Annual IEEE Symposium on Logic in Computer Science, New-Brunswick, CA, June 1996, IEEE Comp. Soc. Press, Los Alamitos (1996)Google Scholar
  48. 48.
    Nieuwenhuis, R., Rubio, A.: Completion of first-order clauses by basic superposition with ordering constraints. Tech. report, Dept. L.S.I., Univ. Polit. Catalunya (1991); To appear in Proc. 11th Conf. on Automated Deduction, Saratoga Springs (1992)Google Scholar
  49. 49.
    Paulin-Mohring, C.: Inductive definitions in the system COQ. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  50. 50.
    Peterson, G.E.: A technique for establishing completeness results in theorem proving with equality. SIAM Journal on Computing 12(1), 82–100 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  51. 51.
    Plaisted, D.A.: Semantic confluence tests and completion methods. Information and Control 65(2-3), 182–215 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  52. 52.
    Shostak, R.E.: An efficient decision procedure for arithmetic with function symbols. J. of the Association for Computing Machinery 26(2), 351–360 (1979)zbMATHMathSciNetGoogle Scholar
  53. 53.
    Shostak, R.E.: Deciding combinations of theories. Technical Report CSL 132, SRI International (February 1982)Google Scholar
  54. 54.
    Wos, L., Robinson, G., Carson, D., Shalla, L.: The concept of demodulation in theorem proving. Journal of the ACM 14, 698–709 (1967)zbMATHCrossRefGoogle Scholar
  55. 55.
    Xi, H., Pfenning, F.: Dependent types in practical programming. In: Conference Record of the 21st Symposium on Principles of Programming Languages, San Antonio, Texas, ACM, New York (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Jean-Pierre Jouannaud
    • 1
  1. 1.LIXÉcole PolytechniquePalaiseauFrance

Personalised recommendations