Skip to main content
SpringerLink
Log in

Research Directions in Rewriting Logic

  • Conference paper
Computational Logic

Part of the book series: NATO ASI Series ((NATO ASI F,volume 165))

Abstract

Rewriting logic expresses an essential equivalence between logic and computation. Systemstatesare in bijective correspondence withformulas, and concurrentcomputationsare in bijective correspondénce withproofs.Given this equivalence between computation and logic, a rewriting logic axiom of the form t → t’ has two readings. Computationally, it means that a fragment of a system’s state that is an instance of the patterntcanchangeto the corresponding instance oft’concurrently with any other state changes; logically, it just means that we can derive the formulat’from the formulat.Rewriting logic is entirely neutral about the structure and properties of the formulas/statest.They are entirelyuser-definableas an algebraic data type satisfying certain equational axioms. Because of this ecumenical neutrality, rewriting logic has, from a logical viewpoint, good properties as alogical framework, in which many other logics can be naturally represented. And, computationally, it has also good properties as asemantic framework, in which many different system styles and models of concurrent computation and many different languages can be naturally expressed without any distorting encodings. The goal of this paper is to provide a relatively gentle introduction to rewriting logic, and to paint in broad strokes the main research directions that, since its introduction in 1990, have been pursued by a growing number of researchers in Europe, the US, and Japan. Key theoretical developments, as well as the main current applications of rewriting logic as a logical and semantic framework, and the work on formal reasoning to prove properties of specifications are surveyed.

FootNote

Supported by Office of Naval Research Contracts N00014-95-C-0225 and N00014-96-C-0114, and by National Science Foundation Grant CCR-9633363.

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 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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. P. Aczel. A general Church-Rosser theorem. Manuscript, University of Manchester, 1978.

    Google Scholar 

  2. G. Agha.Actors.MIT Press, 1986.

    Google Scholar 

  3. G. Agha and C. Hewitt. Concurrent programming using actors. In A. Yonezawa and M. Tokoro, editorsObject-Oriented Concurrent Programmingpages 37–53. MIT Press, 1988.

    Google Scholar 

  4. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems.Theoretical Computer Science138:3–34, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  5. R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R. Grossman, A. Nerode, A. Ravn, and H. Rischel, editorsWorkshop on Theory of Hybrid Systemspages 209–229. Springer LNCS 739, 1993.

    Google Scholar 

  6. R. Alur and D. Dill. The theory of timed automata. In J. de Bakker, G. Huizing, W. P. de Roever, and G. Rozenberg, editorsReal-Time: Theory in Practicevolume 600 of Lecture Notes in Computer Science1991.

    Google Scholar 

  7. A. Asperti. A logic for concurrency. Unpublished manuscript, November 1987.

    Google Scholar 

  8. J.-P. Banâtre and D. L. Metayer. The Gamma model and its discipline of programming.Science of Computer Programming15:55–77, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  9. E. Battiston, V. Crespi, F. D. Cindio, and G. Mauri. Semantic frameworks for a class of modular algebraic nets. In M. Nivat, C. Rattray, T. Russ, and G. Scollo, editorsProc. of the 3rd International AMAST ConferenceWorkshops in Computing. Springer-Verlag, 1994.

    Google Scholar 

  10. M. Bauderon and B. Courcelle. Graph expressions and graph rewriting.Math. Systems Theory20:83–127, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  11. J. Bergstra and J. Tucker. Characterization of computable data types by means of a finite equational specification method. In J. W. de Bakker and J. van Leeuwen, editors, Automata, Languages and Programming, Seventh Colloquium, pages 76–90. Springer-Verlag, 1980. LNCS, Volume 81.

    Chapter  Google Scholar 

  12. G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217–248, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  13. E. Best and R. Devillers. Sequential and concurrent behavior in Petri net theory. Theoretical Computer Science, 55:87–136, 1989.

    Article  MathSciNet  Google Scholar 

  14. M. Bettaz and M. Maouche. How to specify nondeterminism and true concurrency with algebraic term nets. In M. Bidoit and C. Choppy, editorsRecent Trends in Data Type Specificationpages 164–180. Springer LNCS 655, 1993.

    Google Scholar 

  15. M. Bettaz and M. Maouche. Modeling of object based systems with hidden sorted ECATNets. InProc. of MASCOTS’95 Durham North Carolinapages 307–311. IEEE, 1995.

    Google Scholar 

  16. P. Borovanskÿ. Implementation of higher-order unification based on calculus of explicit substitutions. In M. Bartosek, J. Staudek, and J. Wiedermann, editorsProc. SOFTSEM’95pages 363–368. Springer LNCS 1012, 1995.

    Google Scholar 

  17. P. Borovanskÿ, C. Kirchner, and H. Kirchner. Controlling rewriting by rewriting. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  18. P. Borovansky, C. Kirchner, and H. Kirchner. Strategies and rewriting in ELAN. In B. Gramlich and H. Kirchner, editorsProceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville Australia,July 1997)1997.

    Google Scholar 

  19. P. Borovansky, C. Kirchner, and H. Kirchner. Strategies of ELAN: meta-interpretation and partial evaluation. InProceedings of the International Workshop on Theory and Practice of Algebraic Specifications (Amsterdam Holland) 1997.

    Google Scholar 

  20. P. Borovanskÿ, C. Kirchner, H. Kirchner, P.-E. Moreau, and M. Vittek. ELAN: A logical framework based on computational systems. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  21. A. Bouhoula, J.-P. Jouannaud, and J. Meseguer. Specification and proof in membership equational logic. In M. Bidoit and M. Dauchet, editorsProceedings TAPSOFT’97volume 1214 of Lecture Notes in Computer Sciencepages 67–92. Springer-Verlag, 1997.

    Google Scholar 

  22. R. Bruni, J. Meseguer, and U. Montanans. Process and term tile logic. Manuscript, March 1998, SRI International and C.S. Dept., Univ. of Pisa, 1998.

    Google Scholar 

  23. R. Burstall and J. Goguen. The semantics of Clear, a specification language. In D. Bjorner, editorProceedings of the 1979 Copenhagen Winter School on Abstract Software Specificationpages 292–332. Springer LNCS 86, 1980.

    Google Scholar 

  24. CafeOBJ-Project.Proceedings of the CafeOBJ Symposium’98 Numazu Japan. April 1998.

    Google Scholar 

  25. L. Cardelli and A. Gordon. Mobile ambients. Technical report, Digital Equipment Corporation, Systems Research Center, 1997.

    Google Scholar 

  26. C. Castro. An approach to solving binary CSP using computational systems. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  27. K. M. Chandy and J. Misra.Parallel Program Design: A Foundation.Addison-Wesley, 1988.

    Google Scholar 

  28. A. Ciampolini, E. Lamma, P. Mello, and C. Stefanelli. Distributed logic objects: a fragment of rewriting logic and its implementation. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  29. M. Clavel. Reflection in general logics, rewriting logic, and Maude. Ph.D. Thesis, University of Navarre, 1998.

    Google Scholar 

  30. M. Clavel, F. Durán, S. Eker, and J. Meseguer. Building equational logic tools by reflection in rewriting logic. Inin Proc. of the CafeOBJ Symposium ‘88 Numazu, Japan. CafeOBJ Project, April 1998.

    Google Scholar 

  31. M. Clavel, F. Durán, S. Eker, J. Meseguer, and P. Lincoln. An introduction to Maude (beta version). Manuscript, SRI International, March 1998.

    Google Scholar 

  32. M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  33. M. Clavel and J. Meseguer. Axiomatizing reflective logics and languages. In G. Kiczales, editorProceedings of Reflection’96 San Francisco California April 1996pages 263–288. Xerox PARC, 1996.

    Google Scholar 

  34. M. Clavel and J. Meseguer. Reflection and strategies in rewriting logic. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

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

    Google Scholar 

  36. D. Clément, J. Despeyroux, L. Hascoet, and G. Kahn. Natural semantics on the computer. In K. Fuchi and M. Nivat, editorsProceedings France-Japan AI and CS Symposium pages 49–89. ICOT, 1986. Also, Information Processing Society of Japan, Technical Memorandum PL-86–6.

    Google Scholar 

  37. A. Corradini, F. Gadducci, and U. Montanari. Relating two categorical models of term rewriting. In J. Hsiang, editorProc. Rewriting Techniques and Applications Kaiserslauternpages 225–240, 1995.

    Google Scholar 

  38. A. Corradini and U. Montanans. An algebra of graphs and graph rewriting. In D. P. et al., editorCategory Theory and Computer Sciencepages 236–260. Springer LNCS 530, 1991.

    Google Scholar 

  39. B. Courcelle. Graph rewriting: an algebraic and logic approach. In J. van Leeuwen, editorHandbook of Theoretical Computer Science Vol. Bpages 193–242. North-Holland, 1990.

    Google Scholar 

  40. P. Degano, J. Meseguer, and U. Montanans. Axiomatizing net computations and processes. InProc. LICS’89pages 175–185. IEEE, 1989.

    Google Scholar 

  41. P. Degano, J. Meseguer, and U. Montanans. Axiomatizing the algebra of net computations and processes.Acta Informatica33:641–667, 1996.

    MathSciNet  Google Scholar 

  42. .G. Denker. DTL+, A Distributed Temporal Logic Supporting Several Communication Principles. Technical Report, SRI International, Computer Science Laboratory, 333 Ravenswood Ave, Menlo Park, CA 94025, 1998.To appear.

    Google Scholar 

  43. G. Denker and H.-D. Ehrich. Specifying Distributed Information Systems: Fundamentals of an Object-Oriented Approach Using Distributed Temporal Logic. In H. Bowman and J. Derrick, editorsFormal Methods for Open Object-Based Distributed Systems (FMOODS’97) Volume 2 IFIP TC6 WC6.1 Intern. Workshop 21–23 July Canterbury Kent,UKpages 89–104. Chapman & Hall, 1997.

    Google Scholar 

  44. G. Denker and M. Gogolla. Translating TROLLlightconcepts to Maude. In H. Ehrig and F. Orejas, editors,Recent Trends in Data Type Specification, volume 785 ofLNCS, pages 173–187. Springer-Verlag, 1994.

    Chapter  Google Scholar 

  45. G. Denker, J. Meseguer, and C. Talcott. Protocol Specification and Analysis in Maude. In N. Heintze and J. Wing, editorsProc. of Workshop on Formal Methods and Security Protocols 25 June 1998 Indianapolis Indiana1998.

    Google Scholar 

  46. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editorHandbook of Theoretical Computer Science Vol. B pages 243–320. North-Holland, 1990.

    Google Scholar 

  47. R. Diaconescu. Hidden sorted rewriting logic. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.n1/mcs/tcs/pc/volume4.htm

    Google Scholar 

  48. H.-D. Ehrich. Object Specification. Informatik-Bericht 96–07, TU Braunschweig, 1996.

    Google Scholar 

  49. .H.-D. Ehrich, C. Caleiro, A. Sernadas, and G. Denker. Logics for Specifying Concurrent Information Systems. In J. Chornicki and G. Saake, editorsLogics for Databases and Information Systems, pages 167–198. Kluwer Academic Publishers, 1998.

    Google Scholar 

  50. H. Ehrig, H.-J. Kreowski, and G. Rozenberg, editors.Graph Grammars and their Application to Computer Science.Springer LNCS 532, 1991.

    Google Scholar 

  51. S. Eker. Fast matching in combination of regular equational theories. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  52. J. Engelfriet, G. Leih, and G. Rozenberg. Parallel object-based systems and Petri nets, I and II. Technical Report 90–04,90–05, Dept. of Computer Science, University of Leiden, February 1990.

    Google Scholar 

  53. J. Engelfriet, G. Leih, and G. Rozenberg. Net-based description of parallel object-based systems, or POTs and POPs. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editorsFoundations of Object-Oriented Languages Noordwijkerhout The Netherlands May/June 1990pages 229–273. Springer LNCS 489, 1991.

    Chapter  Google Scholar 

  54. M. Fay. First-order unification in an equational theory. InProceedings of the 4th Workshop on Automated Deductionpages 161–167, 1979.

    Google Scholar 

  55. M. Fowler and K. Scott.UML Distilled.Addison-Wesley, 1997.

    Google Scholar 

  56. K. Futatsugi and R. Diaconescu. CafeOBJ report. To appear in the AMAST Series, World Scientific, 1998.

    MATH  Google Scholar 

  57. K. Futatsugi and T. Sawada. Cafe as an extensible specification environment. InProc. of the Kunming International CASE Symposium Kunming China,November1994.

    Google Scholar 

  58. F. Gadducci.On the algebraic approach to concurrent term rewriting.PhD thesis, Dipartimento di Informatica, Università di Pisa, 1996.

    Google Scholar 

  59. F. Gadducci and U. Montanari The tile model. To appear in G. Plotkin, C. Stirling and M. Tofte, eds.Proof Language and Interaction: Essays in Honour of Robin MilnerMIT Press. Also, TR-96–27, C.S. Dept., Univ. of Pisa, 1996.

    Google Scholar 

  60. F. Gadducci and U. Montanari. Enriched categories as models of computation. InProc. 5 th Italian Conference on Theoretical Computer Science Ravello, 1995.

    Google Scholar 

  61. T. Genet. Termination proofs using gpo ordering constraints. In M. Bidoit and M. Dauchet, editorsProceedings 22nd International Colloquium on Trees in Algebra and Programmingvolume 1214 of Lecture Notes in Computer Sciencepages 249–260. Springer-Verlag, 1997.

    Google Scholar 

  62. T. Genet. Proving termination of sequential reduction relation using tree automata. Manuscript; INRIA Lorraine, 1997.

    Google Scholar 

  63. Gérard Berry and Gérard Boudol. The chemical abstract machine InProc. POPL’90pages 81–94. ACM, 1990.

    Google Scholar 

  64. .F. Giunchiglia, C. Pecchiari, and C. Talcott. Reasonig theories: towards an architecture for open mechanized reasoning systems. Technical Report 9409-15, IRST, University of Trento, November 1994. Alsoin Workshop on Frontiers of Combining Systems,FROCOS’96,1996.

    Google Scholar 

  65. J. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations.Theoretical Computer Science105:217–273, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  66. J. Goguen and K. Parsaye-Ghomi. Algebraic denotational semantics using parameterized abstract modules. In J. Diaz and I. Ramos, editorsFormalizing Programming Conceptspages 292–309. Springer-Verlag, 1981. LNCS, Volume 107.

    Chapter  Google Scholar 

  67. J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. Technical Report SRI-CSL-92–03, SRI International, Computer Science Laboratory, 1992. To appear in J.A. Goguen and G.R. Malcolm, editorsApplications of Algebraic Specification Using OBJAcademic Press, 1998.

    Google Scholar 

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

    Google Scholar 

  69. T. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In J. de Bakker, G. Huizing, W. P. de Roever, and G. Rozenberg, editorsReal-Time: Theory in Practicevolume 600 of Lecture Notes in Computer Science1991.

    Google Scholar 

  70. H. Ishikawa, J. Meseguer, T. Watanabe, K. Futatsugi, and H. Nakashima. On the semantics of GAEA-an object-oriented specification of a concurrent reflective language in rewriting logic. InIMSA’97pages 70–109. Information-Technology Promotion Agency, Japan, 1997.

    Google Scholar 

  71. M. Ishisone and T. Sawada. Brute: brute force rewriting engine. Inin Proc. of the CafeOBJ Symposium ‘88 Numazu Japan. CafeOBJ Project, April 1998.

    Google Scholar 

  72. ISO.IS8807: Information Processing Systems - Open System Interconnection - LOTOS - A formal description technique based on the temporal ordering of observational behavior.ISO, February 1989.

    Google Scholar 

  73. ITU-T.Recommendation X.903 - ISO/IEC International Standard 10746–3: “ODP Reference Model: Prescriptive Model”.ISO, 1995.

    Google Scholar 

  74. I. Jacobson, M. Christerson, P. Jonsson, and G. Overgaard.Object-Oriented Software Engineering.Addison-Wesley, 1993.

    Google Scholar 

  75. R. Jagannathan. Dataflow models. In E. Zoyama, editorParallel and Distributed Computing Handbookpages 223–238. McGraw Hill, 1996.

    Google Scholar 

  76. N. Jones. Mix ten year later. InPEPM’95pages 24–38. ACM-SIGPLAN, 1995.

    Google Scholar 

  77. R. Junglclaus, G. Saake, T. Hartmann, and C. Sernadas, editors.Object-oriented specification of information systems: the TROLL language.Technische Universität Braunschweig, Information-Berichte 91–04, 1991.

    Google Scholar 

  78. G. Kelly and R. Street. Review of the elements of 2-categories. In G. Kelly, editorCategory Seminar Sydney 1972/73pages 75–103. Springer Lecture Notes in Mathematics No. 420, 1974.

    Chapter  Google Scholar 

  79. C. Kirchner, H. Kirchner, and M. Vittek. Designing constraint logic programming languages using computational systems. In V. Saraswat and P. van Hentryck, editorsPrinciples and Practice of Constraint Programming: The Newport Paperspages 133–160. MIT Press, 1995.

    Google Scholar 

  80. C. Kirchner and P. Viry. Implementing parallel rewriting. In B. Fronhöfer and G. Wrightson, editorsParallelization in Inference Systemspages 123–138. Springer LNAI 590, 1992.

    Google Scholar 

  81. H. Kirchner and P.-E. Moreau. Prototyping completion with constraints using computational systems. In J. Hsiang, editorProc. Rewriting Techniques and Applications Kaiserslautern1995.

    Google Scholar 

  82. H. Kirchner and P.-E. Moreau. Computational reflection and extension in ELAN. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996.http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  83. A. Knapp. Case studies with CafeOBJ. Inin Proc. of the CafeOBJ Symposium ‘88 Numazu Japan. CafeOBJ Project, April 1998.

    Google Scholar 

  84. P. Kosiuczenko and M. Wirsing. Timed rewriting logic, 1995. Working material for the 1995 Marktoberdorf International Summer School “Logic of Computation”

    Google Scholar 

  85. S. Krogdahl and O. Lysne. Verifying a distributed list system: a case history.Formal Aspects of Computing9:98–118, 1997.

    Article  MATH  Google Scholar 

  86. C. Landauer. Discrete event systems in rewriting logic. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  87. C. Laneve and U. Montanari. Axiomatizing permutation equivalence in the λ-calculus. In H. Kirchner and G. Levi, editorsProc. Third Int. Conf. on Algebraic and Logic Programming Volterra Italy September 1992volume 632 of LNCS, pages 350–363. Springer-Verlag, 1992.

    Chapter  Google Scholar 

  88. C. Laneve and U. Montanari. Axiomatizing permutation equivalence. Mathematical Structures inComputer Science1994. To appear.

    Google Scholar 

  89. F. W. Lawvere. Functor ial semantics of algebraic theories.Proceedings National Academy of Sciences 50:869–873, 1963. Summary of Ph.D. Thesis, Columbia University.

    Article  MathSciNet  MATH  Google Scholar 

  90. U. Lechner. Object-oriented specification of distributed systems in the p-calculus and Maude. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  91. U. Lechner.Object-oriented specification of distributed systems.PhD thesis, University of Passau, 1997.

    Google Scholar 

  92. U. Lechner and C. Lengauer. Modal µ-Maude. InObject Orientation with Parallelism and PersistenceB. Freitag, C.B. Jones, C. Lengauer and H.-J. Schek, editors, Kluwer, 1996.

    Google Scholar 

  93. U. Lechner, C. Lengauer, F. Nickl, and M. Wirsing. How to overcome the inheritance anomaly. inProc.ECOOP’96Springer LNCS, 1996.

    Google Scholar 

  94. U. Lechner, C. Lengauer, and M. Wirsing. An object-oriented airport. In E. Astesiano, G. Reggio, and A. Tarlecki, editorsRecent Trends in Data Type Specification Santa Margherita Italy May/June 1994pages 351–367. Springer LNCS 906, 1995.

    Chapter  Google Scholar 

  95. J. Levy. A higher order unification algorithm for bi-rewriting systems. In J. Agust i and P. Garc ia, editorsSegundo Congreso Programación Declarativapages 291–305, Blanes, Spain, September 1993. CSIC.

    Google Scholar 

  96. .J. Levy and J. Agust i. Bi-rewriting, a term rewriting technique for monotonic order relations. In C. Kirchner, editorProc. Fifth Int. Conf. on Rewriting Techniques and Applications Montreal Canada June 1993, volume 690 of LNCS, pages 17–31. Springer-Verlag, 1993.

    Chapter  Google Scholar 

  97. J.-J. Lévy. Optimal reductions in the lambda calculus. In J. P. Seldin and J. R. Hindley, editorsTo H.B. Curry: Essays on Combinatory Logic Lambda Calculus and Formalismpages 159–191. Academic Press, 1980.

    Google Scholar 

  98. P. Lincoln, N. Mart i-Oliet, and J. Meseguer. Specification, transformation, and programming of concurrent systems in rewriting logic. In G. Blelloch, K. Chandy, and S. Jagannathan, editorsSpecification of Parallel Algorithmspages 309–339. DIMACS Series, Vol. 18, American Mathematical Society, 1994.

    Google Scholar 

  99. P. Lincoln, N. Mart i-Oliet, J. Meseguer, and L. Ricciulli. Compiling rewriting onto SIMD and MIMD/SIMD machines. InProceedings of PARLE’94 6th International Conference on Parallel Architectures and Languages Europepages 37–48. Springer LNCS 817, 1994.

    Google Scholar 

  100. P. Lincoln, J. Meseguer, and L. Ricciulli. The Rewrite Rule Machine Node Architecture and its Performance. InProceedings of CONPAR’94 Linz Austria September 1994pages 509–520. Springer LNCS 854, 1994.

    Google Scholar 

  101. R. Lippmann. An introduction to computing with neural nets.IEEE ASSP Magazinepages 4–22, April 1987.

    Google Scholar 

  102. S. MacLane.Categories for the Working Mathematician.Springer-Verlag, 1971.

    Google Scholar 

  103. N. Marti-Oliet and J. Meseguer. From Petri nets to linear logic. In D. P. et al., editorCategory Theory and Computer Sciencepages 313–340. Springer LNCS 389, 1989. Final version in Mathematical Structures in Computer Science,1:69–101, 1991.

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  105. N. Mart i-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. Technical Report SRI-CSL-93–05, SRI International, Computer Science Laboratory, August 1993. To appear in D. Gabbay, ed.Handbook of Philosophical LogicKluwer Academic Publishers.

    Google Scholar 

  106. N. Mart i-Oliet and J. Meseguer. General logics and logical frameworks. In D. Gabbay, editorWhat is a Logical System?pages 355–392. Oxford University Press, 1994.

    Google Scholar 

  107. N. Mart i-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  108. N. Mart i-Oliet and J. Meseguer. Action and change in rewriting logic. In R. Pareschi and B. Fronhoefer, editorsDynamic Worlds: Prom the Frame Problem to Knowledge Management.1998. To be published by Kluwer Academic Publishers.

    Google Scholar 

  109. I. Mason and C. Talcott. A semantics preserving actor translation. InProc. ICALP’97pages 369–378. Springer LNCS 1256, 1997.

    Google Scholar 

  110. S. Matsuoka and A. Yonezawa. Analysis of inheritance anomaly in object-oriented concurrent programming languages. In G. Agha, P. Wegner, and A. Yonezawa, editorsResearch Directions in Concurrent Object-Oriented Programmingpages 107–150. MIT Press, 1993.

    Google Scholar 

  111. J. Meseguer. General logics. In H.-D. E. et al., editorLogic Colloquium’87pages 275–329. North-Holland, 1989.

    Google Scholar 

  112. J. Meseguer. A logical theory of concurrent objects. InECOOP-OOPSLA’90 Conference on Object-Oriented Programming Ottawa,Canada October 1990pages 101–115. ACM, 1990.

    Google Scholar 

  113. J. Meseguer. Rewriting as a unified model of concurrency. InProceedings of the Concur’90 Conference Amsterdam August 1990pages 384–400. Springer LNCS 458, 1990.

    Google Scholar 

  114. J. Meseguer. Rewriting as a unified model of concurrency. Technical Report SRI-CSL-90–02, SRI International, Computer Science Laboratory, February 1990. Revised June 1990.

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  116. J. Meseguer. A logical theory of concurrent objects and its realization in the Maude language. In G. Agha, P. Wegner, and A. Yonezawa, editorsResearch Directions in Concurrent Object-Oriented Programmingpages 314–390. MIT Press, 1993.

    Google Scholar 

  117. J. Meseguer. Solving the inheritance anomaly in concurrent object-oriented programming. In O. M. Nierstrasz, editorProc. ECOOP’93pages 220–246. Springer LNCS 707, 1993.

    Google Scholar 

  118. J. Meseguer. Rewriting logic as a semantic framework for concurrency: a progress report. InProc. CONCUR’96 Pisa August 1996 pages 331–372. Springer LNCS 1119, 1996.

    Google Scholar 

  119. J. Meseguer. Formal interoperability. InProceedings of the 1998 Conference on Mathematics in Artificial Intelligence Fort Laurerdale Florida January 19981998.http://rutcor.rutgers.edu/~amai/Proceedings.html

    Google Scholar 

  120. J. Meseguer. Membership algebra as a semantic framework for equational specification. in F. Parisi-Presicce, ed., Proc. WADT’97, Springer LNCS 1376, 1998.

    Google Scholar 

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

    Google Scholar 

  122. J. Meseguer and U. Montanari. Petri nets are monoids.Information and Computation88:105–155, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  123. J. Meseguer and U. Montanari. Mapping tile logic into rewriting logic. in F. Parisi-Presicce, ed., Proc. WADT’97, Springer LNCS 1376, 1998.

    Google Scholar 

  124. J. Meseguer and X. Qian. A logical semantics for object-oriented databases. InProc. International SIGMOD Conference on Management of Datapages 89–98. ACM, 1993.

    Google Scholar 

  125. J. Meseguer and C. Talcott. Reasoning theories and rewriting logic. Manuscript, Stanford University, June 1996.

    Google Scholar 

  126. J. Meseguer and C. Talcott. Using rewriting logic to interoperate architectural description languages (I and II). Lectures at the Santa Fe and Seattle DARPAEDCS Workshops, March and July 1997.http://www-formal.stanford.edu/clt/ArpaNsf/adl-interop.html.

    Google Scholar 

  127. J. Meseguer and T. Winkler. Parallel programming in Maude. In J.-P. Banâtre and D. L. Métayer, editorsResearch Directions in High-level Parallel Programming Languagespages 253–293. Springer LNCS 574, 1992. Also Technical Report SRI-CSL-91–08, SRI International, Computer Science Laboratory, November 1991.

    Google Scholar 

  128. R. Milner. Functions as processes.Mathematical Structures in Computer Science2(2):119–141, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  129. S. Morasca, M. Pezze, and M. Trubian. Timed high-level nets.J. of Real-Time Systems3:165–189, 1991.

    Article  Google Scholar 

  130. P.-E. Moreau and H. Kirchner. Compilation techniques for associative-commutative normalisation. InProceedings of the International Workshop on Theory and Practice of Algebraic Specifications (Amsterdam Holland)1997.

    Google Scholar 

  131. P. Mosses.Action Semantics.Cambridge University Press, 1992.

    Book  Google Scholar 

  132. E. Najm and J.-B. Stefani. Computational models for open distributed systems. In H. Bowman and J. Derrick, editorsFormal Methods for Open Object-based Distributed Systems Vol. 2pages 157–176. Chapman & Hall, 1997.

    Google Scholar 

  133. S. Nakajima. Encoding mobility in CafeOBJ: an exercise of describing mobile code-based software architecture. Inin Proc. of the CafeOBJ Symposium ‘88 Numazu Japan. CafeOBJ Project, April 1998.

    Google Scholar 

  134. S. Nakajima and K. Futatsugi. An object-oriented modeling method for algebraic specifications in CafeOBJ. InProceedings 19th International Conference on Software Engineering pages 34–44. IEEE Computer Society Press, May 1997.

    Google Scholar 

  135. H. Nakashima. Organic programming for situation-thick AI systems. InIMSA ‘87pages 156–163. Information-Technology Promotion Agency, Japan, 1997.

    Google Scholar 

  136. K. Ogata and K. Futatsugi. An abstract machine for order-sorted conditional term rewriting systems. In H. Comon, editorProceedings of the 8th Conference on Rewriting Techniques and Applications.Springer LNCS 1232, 1997.

    Google Scholar 

  137. K. Ohmaki, K. Futatsugi, and K. Takahashi. A basic LOTOS simulator in OBJ. InProceedings of the International Conference of Information Technology Commemorating the 30th Anniversary of the Information Processing Society of Japan (InfoJapan’90)pages 497–504. IPSJ, October 1990.

    Google Scholar 

  138. P. C. Olveczky, P. Kosiuczenko, and M. Wirsing. An object-oriented algebraic steam-boiler control specification. In J.-R. Abrial, E. Börger, and H. Langmaack, editorsThe Steam-Boiler Case Study Book.Springer-Verlag, 1996. To appear.

    Google Scholar 

  139. P. C. Olveczky and J. Meseguer. Specifying real-time systems in rewriting logic. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  140. I. Pita and N. Mart i-Oliet. A Maude specification of an object oriented database model for telecomunication networks. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.n1/mcs/tcs/pc/volume4.htm

    Google Scholar 

  141. G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Dept., Aarhus University, 1981.

    Google Scholar 

  142. J.-C. Raoult and F. Voisin. Set-theoretic graph rewriting. In H.-J. Schneider and H. Ehrig, editorsGraph Transformations in Computer Sciencepages 312–325. Springer LNCS 776, 1994.

    Google Scholar 

  143. H. Reichel. An approach to object semantics based on terminal co-algebras. To appear inMathematical Structures in Computer Science1995. Presented atDagstuhl Seminar on Specification and SemanticsSchloss Dagstuhl, Germany, May 1993.

    Google Scholar 

  144. W. Reisig.Petri Nets.Springer-Verlag, 1985.

    Google Scholar 

  145. C. Ringeissen. Prototyping combination of unification algorithms with the ELAN rule-based programming language. In H. Comon, editorProceedings of the 8th Conference on Rewriting Techniques and Applications.Springer LNCS 1232, 1997.

    Google Scholar 

  146. G. Saake and A. Sernadas, editors.Information Systems-Correctness and Reusability.Technische Universität Braunschweig, Information-Berichte 91–03, 1991.

    Google Scholar 

  147. H.-J. Schneider and H. Ehrig, editors.Graph Transformations in Computer Science.Springer LNCS 776, 1994.

    Google Scholar 

  148. M. Schorlemmer. Bi-rewriting rewriting logic. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996.http://wwwi.elsevier.nl/mcs/tcs/pc/volume4.htmhtm.

    Google Scholar 

  149. M. Shaw and D. Garlan.Software Architecture.Prentice Hall, 1996.

    Google Scholar 

  150. M.-O. Stehr. A rewriting semantics for algebraic Petri nets. Manuscript, March 1998, SRI International and C.S. Dept., Univ. of Hamburg, 1998.

    Google Scholar 

  151. J. Stell. Modelling term rewriting systems by sesqui-categories. Technical Report TR94–02, Keele University, 1994. Also in shorter form in Proc. C.A.E.N., 1994, pp. 121–127.

    Google Scholar 

  152. C. L. Talcott. An actor rewrite theory. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.n1/mcs/tcs/pc/volume4.htm

    Google Scholar 

  153. C. L. Talcott. Interaction semantics for components of distributed systems. In E. Najm and J.-B. Stefani, editorsFormal Methods for Open Object-based Distributed Systemspages 154–169. Chapman & Hall, 1997.

    Google Scholar 

  154. V. F. Turchin. The concept of a supercompiler.ACM Transactions on Programming Languages and Systems8(3):292–325, 1986.

    Article  MathSciNet  MATH  Google Scholar 

  155. V. F. TurchinRefal-5: programming guide and referencemanual. New England Publishing Co., 1989.

    Google Scholar 

  156. W. van der Aalst. Interval timed coloured Petri nets and their analysis. In M. A. Marsan, editorApplication and Theory of Petri Nets 1993pages 453–472. Springer LNCS 691, 1993.

    Google Scholar 

  157. A. van Deursen.ExecutableLanguageDefinitions.PhD thesis, University of Amsterdam, 1994.

    Google Scholar 

  158. P. Viry. Rewriting: An effective model of concurrency. In C. Halatsis et al., editorsPARLE’94 Proc. Sixth Int. Conf. on Parallel Architectures and Languages Europe Athens Greece July 1994volume 817 of LNCS pages 648–660. Springer-Verlag, 1994.

    Google Scholar 

  159. P. Viry. Input/output for ELAN. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  160. M. Vittek.ELAN: Un cadre logique pour le prototypage de langages de programmation avec contraintes.PhD thesis, Université Henry Poincaré — Nancy I, 1994.

    Google Scholar 

  161. M. Wand and D. Friedman. The mystery of the tower revealed.Lisp and Symbolic Computation1(1):11–38, 1988.

    Article  Google Scholar 

  162. M. Wirsing and A. Knapp. A formal approach to object-oriented software enginering. In J. Meseguer, editorProc. First Intl. Workshop on Rewriting Logic and its Applicationsvolume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. http://wwwl.elsevier.nl/mcs/tcs/pc/volume4.htm

    Google Scholar 

  163. M. Wirsing, F. Nicki, and U. Lechner. Concurrent object-oriented design specification in SPECTRUM. Technical report, Institut für Informatik, Universität München, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International 333 Ravenswood Ave, 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 Mathematics, University of Munich, Theresienstr. 39, Munich, D-80333, Germany

    Ulrich Berger  & Helmut Schwichtenberg  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Meseguer, J. (1999). Research Directions in Rewriting Logic. In: Berger, U., Schwichtenberg, H. (eds) Computational Logic. NATO ASI Series, vol 165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-58622-4_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-58622-4_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-63670-7

  • Online ISBN: 978-3-642-58622-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation