Rewriting logic and maude: Concepts and applications

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

For the most part, rewriting techniques have been developed and applied to support efficient equational reasoning and equa-tional specification, verification, and programming. Therefore, a rewrite rule t — 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 — t', one computational, and another logical: (i) computationally, the rewrite rule t — t' is interpreted as a local transition in a concurrent system; (ii) logically, the rewrite rule t — 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.

Original languageEnglish (US)
Title of host publicationRewriting Techniques and Applications - 11th International Conference, RTA 2000, Proceedings
EditorsLeo Bachmair
PublisherSpringer-Verlag Berlin Heidelberg
Pages1-26
Number of pages26
ISBN (Electronic)354067778X, 9783540677789
DOIs
StatePublished - 2000
Externally publishedYes
Event11th International Conference on Rewriting Techniques and Applications, RTA 2000 - Norwich, United Kingdom
Duration: Jul 10 2000Jul 12 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1833
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other11th International Conference on Rewriting Techniques and Applications, RTA 2000
CountryUnited Kingdom
CityNorwich
Period7/10/007/12/00

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Rewriting logic and maude: Concepts and applications'. Together they form a unique fingerprint.

Cite this