Rewriting logic is a simple computational logic that can naturally express both concurrent
computation and logical deduction with great generality. This paper provides a gentle …

The theory and applications of rewriting logic have been vigorously developed by
researchers all over the world during the past eleven years. The attached bibliography …

This chapter describes some existing Maude-based tools that are available for download.
The first section describes tools concerned with analysis of either Maude specifications, or of …

This paper proposes membership equational logic—a Horn logic in which the basic
predicates are equations t= t′ and membership assertions t: s stating that a term t belongs …

This is an introduction to the philosophy and use of OBJ, emphasizing its oper-ational
semantics, with aspects of its history and its logical semantics. Release 2 of OBJ3 is …

Program transformation is used in many areas of software engineering. Examples include
compilation, optimization, synthesis, refactoring, migration, normalization and improvement …

Rewriting logic [40] is proposed as a logical framework in which other logics can be
represented, and as a semantic framework for the specification of languages and systems …

This paper introduces the basic concepts of the rewriting logic language Maude and
discusses its implementation. Maude is a wide-spectrum language supporting formal …

This introduction tries to give the big picture on the goals, design philosophy, logical
foundations, applications, and overall structure of Maude. It is written in an impressionistic …

Program transformation is used in a wide range of applications including compiler
construction, optimization, program synthesis, refactoring, software renovation, and reverse …