TY - GEN
T1 - Rewriting logic and maude
T2 - 11th International Conference on Rewriting Techniques and Applications, RTA 2000
AU - Meseguer, José
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.
PY - 2000
Y1 - 2000
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84937406532&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84937406532&partnerID=8YFLogxK
U2 - 10.1007/10721975_1
DO - 10.1007/10721975_1
M3 - Conference contribution
AN - SCOPUS:84937406532
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 26
BT - Rewriting Techniques and Applications - 11th International Conference, RTA 2000, Proceedings
A2 - Bachmair, Leo
PB - Springer
Y2 - 10 July 2000 through 12 July 2000
ER -