Skip to main content
SpringerLink
Log in

Rewriting Logic and Maude: Concepts and Applications

  • Conference paper
Rewriting Techniques and Applications (RTA 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1833))

Included in the following conference series:

Abstract

For the most part, rewriting techniques have been developed and applied to support efficient equational reasoning and equational specification, verification, and programming. Therefore, a rewrite rule \(t \longrightarrow t'\) has been usually interpreted as a directed equation t = t ’. Rewriting logic is a substantial broadening of the semantics given to rewrite rules. The equational reading is abandoned, in favor of a more dynamic interpretation. There are now in fact two complementary readings of a rule \(t \longrightarrow t'\), one computational, and another logical: (i) computationally, the rewrite rule \(t \longrightarrow t'\) is interpreted as a local transition in a concurrent system; (ii) logically, the rewrite rule \(t \longrightarrow t'\) is interpreted as an inference rule. The experience gained so far strongly suggest that rewriting is indeed a very flexible and general formalism for both computational and logical applications. This means that from the computational point of view rewriting logic is a very expressive semantic framework, in which many different models of concurrency, languages, and distributed systems can be specified and programmed; and that from a logical point of view is a general logical framework in which many different logics can be represented and implemented. This paper introduces the main concepts of rewriting logic and of the Maude rewriting logic language, and discusses a wide range of semantic framework and logical framework applications that have been developed in rewriting logic using Maude.

Supported by DARPA through Rome Laboratories Contract F30602-C-0312, by DARPA and NASA through Contract NAS2-98073, by Office of Naval Research Contract N00014-99-C-0198, and by National Science Foundation Grant CCR-9900334.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allen, R., Garlan, D.: Formalizing architectural connection. In: Proceedings 16th International Conference on Software Engineering (1994)

    Google Scholar 

  2. Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Soft. Eng. and Meth. (July 1997)

    Google Scholar 

  3. Asperti, A.: A logic for concurrency. Unpublished manuscript (November 1987)

    Google Scholar 

  4. Barendregt, H.P.: Lambda-calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T. (eds.) Background: Computational Structures. Handbook of Logic in Computer Science, vol. 2. Clarendon Press, Oxford (1992)

    Google Scholar 

  5. Basin, D., Clavel, M., Meseguer, J.: Reflective metalogical frameworks. In: Proc. LFM 1999, Paris, France (September 1999) http://www.cs.bell-labs.com/~felty/LFM99/

  6. Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. http://www.informatik.uni-freiburg.de/~basin/pubs/pubs.html

  7. Bergstra, J., Tucker, J.: Characterization of computable data types by means of a finite equational specification method. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming, Seventh Colloquium. LNCS, vol. 81, pp. 76–90. Springer, Heidelberg (1980)

    Google Scholar 

  8. Blanqui, F., Jouannaud, J., Okada, M.: The calculus of algebraic constructions. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, p. 301. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Borovanský, P., Kirchner, C., Kirchner, H.: Controlling rewriting by rewriting. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  10. Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E., Vittek, M.: ELAN: A logical framework based on computational systems. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  11. Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  12. Braga, C., Haeusler, H., Meseguer, J., Mosses, P.: Maude Action Tool: using reflection to map action semantics to rewriting logic. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, p. 407. Springer, Heidelberg (2000) (to appear)

    Chapter  Google Scholar 

  13. Bruni, R., Meseguer, J., Montanari, U.: Internal strategies in a rewriting implementation of tile systems. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, North Holland, Amsterdam (1998)

    Google Scholar 

  14. Bruni, R., Meseguer, J., Montanari, U.: Process and term tile logic. Technical Report SRI-CSL 1998-06, SRI International (July 1998)

    Google Scholar 

  15. Bruni, R., Meseguer, J., Montanari, U.: Executable tile specifications for process calculi. In: Finance, J.-P. (ed.) FASE 1999. LNCS, vol. 1577, pp. 60–76. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Burstall, R., Goguen, J.A.: The semantics of Clear, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980)

    Google Scholar 

  17. Carabetta, G., Degano, P., Gadducci, F.: CCS semantics via proved transition systems and rewriting logic. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, North Holland, Amsterdam (1998)

    Google Scholar 

  18. Clavel, M.: Reflection in general logics and in rewriting logic, with applications to the Maude language. Ph.D. Thesis, University of Navarre (1998)

    Google Scholar 

  19. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. SRI International (January 1999), http://maude.csl.sri.com

  20. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: A tutorial on Maude. SRI International (March 2000), http://maude.csl.sri.com

  21. Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: Proc. of the CafeOBJ Symposium 1998, Numazu, Japan, April 1998, CafeOBJ Project (1998), http://maude.csl.sri.com

  22. Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)

    Google Scholar 

  23. Clavel, M., Meseguer, J.: Reflection and strategies in rewriting logic. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  24. Clavel, M., Meseguer, J.: Internal strategies in a reflective logic. In: Gramlich, B., Kirchner, H. (eds.) Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville, Australia), pp. 1–12 (July 1997)

    Google Scholar 

  25. Clavel, M., Meseguer, J.: Reflection in conditional rewriting logic. Submitted for publication (2000)

    Google Scholar 

  26. Constable, R.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1987)

    Google Scholar 

  27. Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2/3), 95–120 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  28. Corradini, A., Gadducci, F., Montanari, U.: Relating two categorical models of term rewriting. In: Hsiang, J. (ed.) Proc. Rewriting Techniques and Applications, Kaiserslautern, pp. 225–240 (1995)

    Google Scholar 

  29. Degano, P., Meseguer, J., Montanari, U.: Axiomatizing the algebra of net computations and processes. Acta Informatica 33, 641–667 (1996)

    MathSciNet  Google Scholar 

  30. Denker, G., Meseguer, J., Talcott, C.: Protocol Specification and Analysis in Maude. In: Heintze, N., Wing, J. (eds.) Proc. of Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana, June 25 (1998), http://www.cs.bell-labs.com/who/nch/fmsp/index.html

  31. Denker, G., Meseguer, J., Talcott, C.: Rewriting Semantics of Distributed Meta Objects and Composable Communication Services (1999) (working draft)

    Google Scholar 

  32. Denker, G., Meseguer, J., Talcott, C.: Formal specification and analysis of active networks and communication protocols: the Maude experience. In: Proc. DARPA Information Survivability Conference and Exposition DICEX 2000, Hilton Head, South Carolina, vol. 1, pp. 251–265. IEEE, Los Alamitos (2000)

    Chapter  Google Scholar 

  33. Denker, G., Millen, J.: CAPSL Intermediate Language. In: Heintze, N., Clarke, E. (eds.) Workshop on Formal Methods and Security Protocols (FMSP 1999), Trento, Italy (part of FLOC 1999), July 5 (1999), http://cm.bell-labs.com/cm/cs/who/nch/fmsp99/

  34. Denker, G., Garcia-Luna-Aceves, J.J., Meseguer, J., Ölveczky, P., Raju, J., Smith, B., Talcott, C.: Specification and Analysis of a Reliable Broadcasting Protocol in Maude. In: Hajek, B., Sreenivas, R. (eds.) Proc. 37th Allerton Conference on Communication, Control and Computation (1999), http://www.comm.csl.uiuc.edu/allerton

  35. Durán, F.: A reflective module algebra with applications to the Maude language. Ph.D. Thesis, University of Málaga (1999)

    Google Scholar 

  36. Durán, F.,Eker, S., Lincoln, P., Meseguer, J.: Principles of Mobile Maude. SRI International (March 2000), http://maude.csl.sri.com

  37. Durán, F., Meseguer, J.: An extensible module algebra for Maude. In: Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS, North Holland, Amsterdam (1998)

    Google Scholar 

  38. Eker, S.: Fast matching in combination of regular equational theories. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  39. Futatsugi, K., Diaconescu, R.: CafeOBJ report. AMAST Series. World Scientific, Singapore (1998)

    MATH  Google Scholar 

  40. Gadducci, F., Montanari, U.: The tile model. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, Cambridge (1996); Also, TR-96-27, C.S. Dept., Univ. of Pisa

    Google Scholar 

  41. Girard, J.-Y.: Linear Logic. Theoretical Computer Science 50, 1–102 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  42. Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105, 217–273 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  43. Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, Dordrecht (2000)

    Google Scholar 

  44. Gordon, M.: Introduction to HOL: A Theorem Proving Environment. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  45. Gunter, C., Gehlot, V.: Nets as tensor theories. Technical Report MS-CIS-89-68, Dept. of Computer and Information Science, University of Pennsylvania (1989)

    Google Scholar 

  46. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association Computing Machinery 40(1), 143–184 (1993)

    MATH  MathSciNet  Google Scholar 

  47. Hicks, M., Kakkar, P., Moore, J.T., Gunter, C.A., Nettles, S.: PLAN: A Packet Language for Active Networks. In: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming Languages, pp. 86–93. ACM, New York (1998)

    Chapter  Google Scholar 

  48. Hoare, C.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  49. Howe, D.J.: Semantical foundations for embedding HOL in Nuprl. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 85–101. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  50. Jouannaud, J.P.: Membership equational logic, calculus of inductive constructions, and rewrite logic. In: 2nd Workshop on Rewrite Logic and Applications (1998)

    Google Scholar 

  51. Kirchner, C., Kirchner, H. (eds.): Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications. ENTCS. North Holland, Amsterdam (1998)

    Google Scholar 

  52. Kirchner, C., Kirchner, H., Vittek, M.: Designing constraint logic programming languages using computational systems. In: Saraswat, V., van Hentenryck, P. (eds.) Principles and Practice of Constraint Programming: The Newport Papers, pp. 133–160. MIT Press, Cambridge (1995)

    Google Scholar 

  53. Laneve, C., Montanari, U.: Axiomatizing permutation equivalence. Mathematical Structures in Computer Science 6, 219–249 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  54. Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, Oxford (1994)

    Google Scholar 

  55. Magnussen, L.: The Implementation of ALF - a Proof Editor based on Martin-Löf ’s Monomorphic Type Theory with Explicit Substitutions. PhD thesis, University of Göteborg, Dept. of Computer Science (1994)

    Google Scholar 

  56. Martí-Oliet, N., Meseguer, J.: From Petri nets to linear logic. In: Dybjer, P., Pitts, A.M., Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 389, pp. 313–340. Springer, Heidelberg (1989); Final version in Mathematical Structures in Computer Science 1, 69–101, (1991)

    Chapter  Google Scholar 

  57. Martí-Oliet, N., Meseguer, J.: From Petri nets to linear logic through categories: a survey. Intl. J. of Foundations of Comp. Sci. 2(4), 297–399 (1991)

    Article  MATH  Google Scholar 

  58. Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. Technical Report SRI-CSL-93-05, SRI International, Computer Science Laboratory. To appear in Gabbay, D. (ed.) Handbook of Philosophical Logic, Kluwer Academic Publishers, Dordrecht (1993)

    Google Scholar 

  59. Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996)

    Google Scholar 

  60. Meseguer, J.: General logics. In: Ebbinghaus, H.-D., et al. (eds.) Logic Colloquium 1987, pp. 275–329. North-Holland, Amsterdam (1989)

    Google Scholar 

  61. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  62. Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314–390. MIT Press, Cambridge (1993)

    Google Scholar 

  63. Meseguer, J.: Rewriting logic as a semantic framework for concurrency: a progress report. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)

    Google Scholar 

  64. Meseguer, J. (ed.): Proc. First Intl. Workshop on Rewriting Logic and its Applications. ENTCS. North Holland, Amsterdam (1996)

    Google Scholar 

  65. Meseguer, J.: Membership algebra as a semantic framework for equational speci-fication. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)

    Google Scholar 

  66. Meseguer, J.: Research directions in rewriting logic. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, 1997. Springer, Heidelberg (1999)

    Google Scholar 

  67. Meseguer, J., Futatsugi, K., Winkler, T.: Using rewriting logic to specify, program, integrate, and reuse open concurrent systems of cooperating agents. In: Proceedings of the 1992 International Symposium on New Models for Software Architecture, Tokyo, Japan. pp. 61–106, Research Institute of Software Engineering (November 1992)

    Google Scholar 

  68. Meseguer, J., Montanari, U.: Petri nets are monoids. Information and Computation 88, 105–155 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  69. Meseguer, J., Montanari, U.: Mapping tile logic into rewriting logic. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376. Springer, Heidelberg (1998)

    Google Scholar 

  70. Meseguer, J., Talcott, C.: A partial order event model for concurrent objects. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 415–430. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  71. Mosses, P.: Action Semantics. Cambridge University Press, Cambridge (1992)

    Book  MATH  Google Scholar 

  72. Mosses, P.: Foundations of modular SOS. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 70–80. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  73. Najm, E., Stefani, J.-B.: Computational models for open distributed systems. In: Bowman, H., Derrick, J. (eds.) Formal Methods for Open Object-based Distributed Systems, vol. 2, pp. 157–176. Chapman & Hall, Boca Raton (1997)

    Google Scholar 

  74. Nakajima, S.: Encoding mobility in CafeOBJ: an exercise of describing mobile codebased software architecture. In: Proc. of the CafeOBJ Symposium 1998, Numazu, Japan. CafeOBJ Project (April 1998)

    Google Scholar 

  75. Ölveczky, P.C., Meseguer, J.: Specifying real-time systems in rewriting logic. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  76. Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Submitted for publication (1999)

    Google Scholar 

  77. Paulin-Mohring, C.: Inductive Definitions in the system Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  78. Pita, I., Martí-Oliet, N.: A Maude specification of an object oriented database model for telecommunication networks. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  79. Pita, I., Martí-Oliet, N.: Using reflection to specify transaction sequences in rewriting logic. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol. 1589, pp. 261–276. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  80. Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 313–332. Springer, Heidelberg (1994)

    Google Scholar 

  81. Reisig, W.: Petri Nets. Springer, Heidelberg (1985)

    MATH  Google Scholar 

  82. Stehr, M.-O.: A rewriting semantics for algebraic nets. In: Girault, C., Valk, R. (eds.) Petri Nets for System Engineering - A Guide to Modelling, Verification, and Applications, Springer, Heidelberg (to appear)

    Google Scholar 

  83. Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic. In: Proc. of LFM 1999: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28 (1999)

    Google Scholar 

  84. Stehr, M.-O., Naumov, P., Meseguer, J.: A proof-theoretic approach to the HOL-Nuprl connection with applications to proof translation. Manuscript, SRI International (February 2000) http://www.csl.sri.com/~stehr/fi_eng.html,

  85. Talcott, C.L.: An actor rewrite theory. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  86. Talcott, C.L.: Interaction semantics for components of distributed systems. In: Najm, E., Stefani, J.-B. (eds.) Formal Methods for Open Object-based Distributed Systems, pp. 154–169. Chapman & Hall, Boca Raton (1997)

    Google Scholar 

  87. Talcott, C.L.: Actor theories in rewriting logic. Submitted for publication (1999)

    Google Scholar 

  88. Verdejo, A., Martí-Oliet, N.: Executing and verifying CCS in Maude. Technical Report 99-00, Dto. Sistemas Informáticos y Programación, Universidad Complutense, Madrid; also, http://maude.csl.sri.com

  89. Viry, P.: Rewriting modulo a rewrite system. TR-95-20, C.S. Department, University of Pisa (1996)

    Google Scholar 

  90. Viry, P.: Rewriting: An effective model of concurrency. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 648–660. Springer, Heidelberg (1994)

    Google Scholar 

  91. Viry, P.: Input/output for ELAN. In: Meseguer, J. (ed.) Proc. First Intl.Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

  92. Wang, B.-Y., Meseguer, J., Gunter, C. A.: Specification and formal analysis of a PLAN algorithm in Maude. To appear in Proc. DSVV (2000)

    Google Scholar 

  93. Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. In: Meseguer, J. (ed.) Proc. First Intl. Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier, Amsterdam (1996), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International, Menlo Park, CA, 94025, USA

    José Meseguer

Authors
  1. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Stony Brook University, Stony Brook, P.O. Box, New York

    Leo Bachmair

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Meseguer, J. (2000). Rewriting Logic and Maude: Concepts and Applications. In: Bachmair, L. (eds) Rewriting Techniques and Applications. RTA 2000. Lecture Notes in Computer Science, vol 1833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721975_1

Download citation

  • DOI: https://doi.org/10.1007/10721975_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67778-9

  • Online ISBN: 978-3-540-44980-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation