RDP

MEETINGS

VENUE
 RTA'03 14th International Conference on Rewriting Techniques and Applications Valencia, Spain, June 9-11, 2003

ABSTRACTS OF REGULAR PAPERS ACCEPTED FOR PRESENTATION

Rewriting Modulo in Deduction Modulo
F. Blanqui (École Polytechnique, Palaiseau, France)

We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous work, we defined general syntactic conditions based on the notion of computable closure for ensuring the termination of the combination of rewriting and $\b$-reduction. Here, we show that this result is preserved when considering rewriting modulo a set of equations if the equivalence classes generated by these equations are finite, the equations are linear and satisfy general syntactic conditions also based on the notion of computable closure. This includes equations like associativity and commutativity, and provides an original treatment of termination modulo equations.

Validation of the JavaCard Platform with Implicit Induction Techniques
G. Barthe (INRIA Sophia-Antipolis, France)
S. Stratulat (Université de Metz, France)

The bytecode verifier (BCV), which performs a static analysis to reject potentially insecure programs, is a key security function of the Java(Card) platform. Over the last few years there have been numerous projects to prove formally the correctness of bytecode verification, but relatively little effort has been made to provide methodologies, techniques and tools that help such formalisations. In earlier work, we develop a methodology and a specification environment featuring a neutral mathematical language based on conditional rewriting, that considerably reduce the cost of specifying virtual machines. In this work, we show that such a neutral mathematical language based on conditional rewriting is also beneficial for performing automatic verifications on the specifications, and illustrate in particular how implicit induction techniques can be used for the validation of the Java(Card) Platform. More precisely, we report on the successful use of SPIKE, a first-order theorem prover based on implicit induction, (1) to cross-validate virtual machines, including a reference virtual machine which performs saftey checks at run-time, an offensive virtual machine which does not, and an abstract virtual machine that is used by the BCV; (2) to show that the abstract virtual machine is monotone w.r.t. the order induced by the subclass and subinterface relation. Both results are crucial to establish the correctness of the BCV.

XML Schema, Tree Logic and Sheaves Automata
S. Dal Zilio (CNRS, Marseille, France)
D. Lugiez (Université de Provence, Marseille, France)

XML documents, and other forms of semi-structured data, may be roughly described as edge labeled trees, it is therefore natural to use tree automata to reason on them. This idea has already been successfully applied in the context of Document Type Definition (DTD), the simplest standard for defining XML documents validity, but additional work is needed to take into account XML Schema, a more advanced standard, for which regular tree automata are not satisfactory. A major reason for this inadequacy is the presence of an associative-commutative operator in the schema language, inherited from the &-operator of SGML, and the inherent limitations of regular tree automata in dealing with associative-commutative algebras. In this paper, we define a tree logic that directly embeds XML Schema as a plain subset and that explicitly takes into account the equational properties of the schema operators. Namely associativity of sequential composition and associativity-commutativity of &. Another contribution is a new class of automata for unranked trees, used to decide our logic, that is well-suited to the processing of XML documents and schemas. We believe it is the first work applying tree automata to XML that considers the &-operator. This addition is significant because this operator has been the subject of many controversial debates among the XML community and because it poses several difficult implementation problems. Our work provides some justifications for these difficulties and gives several complexity results on problems related to XML schema, such as checking that a document conform to a schema, checking whether the set of documents matching a schema is empty, ... Among other results, we also make clear how simple syntactical restrictions on schemas improve the complexity of simple operations.

Termination of String Rewriting Rules That Have One Pair of Overlaps
A. Geser (National Institute of Aerospace, Hampton, USA)

This paper presents a partial solution to the long standing open problem of termination of one-rule string rewriting. Overlaps between the two sides of the rule play a central role in existing termination criteria. We characterize termination of all one-rule string rewriting systems that have one such overlap at either end. This both completes a result of Kurth and generalizes a result of Shikishima-Tsuji et al.

New decidability results for fragments of first order logic and application to cryptographic protocols
H. Comon-Lundh (ENS Cachan, France)
V. Cortier (ENS Cachan, France)

We consider a new extension of the Skolem class for first-order logic and prove its decidability by resolution techniques. We then extend this class including the built-in equational theory of exclusive or. Again, we prove the decidability of the class by resolution techniques. Considering such fragments of first-order logic is motivated by the automatic verification of cryptographic protocols, for an arbitrary number of sessions; the first-order formalization is an approximation of the set of possible traces, for instance relaxing the nonce freshness assumption. As an application of the decision results for extensions of the Skolem class, we get some new decidability results for the verification of cryptographic protocols without the perfect cryptography assumption: we may include the algebraic properties of exclusive or. The proof of our main result relies on classical techniques: ordered strategies, narrowing modulo AC, semantic trees.

Associative-Commutative Rewriting on Large Terms
S. Eker (SRI International, Menlo Park, USA)

We introduce a novel representation for associative-commutative (AC) terms which, for certain important classes of rewrite rule, allows both the AC matching and the AC renormalization steps to be accomplished using time and space that is logarithmic in the size of the flattened AC argument lists involved. This novel representation can be cumbersome for other, more general algorithms and manipulations. Hence, we describe machine efficient techniques for converting to and from a more conventional representation together with a heuristic for deciding at runtime when to convert a term to the new representation. We sketch how our approach can be generalized to order-sorted AC rewriting and to other equational theories. We also present some experimental results using the Maude 2 interpreter.

Recognizing Boolean Closed A-Tree Languages with Membership Conditional Rewriting Mechanism
H. Ohsaki (AIST & JST, Amagasaki, Japan)
H. Seki (Nara Institute of Science and Technology, Ikoma, Japan)
T. Takai (AIST, Amagasaki, Japan)

This paper provides an algorithm to compute the complement of tree languages recognizable with A-TA (tree automata with associativity axioms). Due to this closure property together with the previously obtained results, we know that the class is boolean closed, while keeping recognizability of A-closures of regular tree languages. In the proof of the main result, a new framework of tree automata, called sequence-tree automata, is introduced as a generalization of Lugiez and Dal Zilio's multi-tree automata of an associativity case. It is also shown that recognizable A-tree languages are closed under a one-step rewrite relation in case of ground A-term rewriting. This result allows us to compute an under-approximation of A-rewrite descendants of recognizable A-tree languages with arbitrary accuracy.

Termination of Simply Typed Term Rewriting Systems by Translation and Labelling
T. Aoto (Tohoku University, Sendai, Japan)
T. Yamada (Mie University, Tsu, Japan)

Simply typed term rewriting proposed by Yamada (RTA 2001) is a framework of term rewriting allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed term rewriting dispenses with bound variables. This paper presents a method for proving termination of simply typed term rewriting systems (STTRSs, for short). We first give a translation of STTRSs into many-sorted first-order TRSs and shows that termination problem of STTRSs is reduced to that of many-sorted first-order TRSs. Next, we introduce a labelling method which is applied to first-order TRSs obtained by the translation to facilitate termination proof of them; our labelling employs an extension of semantic labelling where terms are interpreted on a many-sorted algebra.

Liveness in Rewriting
J. Giesl (RWTH Aachen, Germany)
H. Zantema (Eindhoven University of Technology, Eindhoven, The Netherlands)

In this paper, we show how the problem of verifying liveness properties is related to termination of term rewrite systems (TRSs). We formalize liveness in the framework of rewriting and present a sound and complete transformation to transform liveness problems into TRSs. Then the transformed TRS terminates if and only if the original liveness property holds. This shows that liveness and termination are essentially equivalent. To apply our approach in practice, we introduce a simpler sound transformation which only satisfies the only if'-part. By refining existing techniques for proving termination of TRSs we show how liveness properties can be verified automatically. As examples, we prove a liveness property of a waiting line protocol for a network of processes and a liveness property of a protocol on a ring of processes.

Rewriting Logic and Probabilities
O. Bournez (INRIA, Villers-lés-Nancy, France)
M. Hoyrup (ENS Lyon, France)

Rewriting Logic has shown to provide a general and elegant framework for unifying a wide variety of models, including concurrency models and deduction systems. In order to extend the modeling capabilities of rule based languages, it is natural to consider that the firing of rules can be subject to some probabilistic laws. Considering rewrite rules subject to probabilities leads to numerous questions about the underlying notions and results. In this paper, we discuss whether there exists a notion of probabilistic rewrite system with an associated notion of probabilistic rewriting logic.

Efficient Reductions with Director Strings
F.-R. Sinot (King's College, London, United Kingdom)
M. Fernández (King's College, London, United Kingdom)
I. Mackie (King's College, London, United Kingdom)

We present a name free lambda-calculus with explicit substitutions based on a generalized notion of director strings: we annotate a term with information about how each substitution should be propagated through the term. We define a first calculus which implements closed reduction and is adequate for the evaluation of programs (reduction to weak head normal form). In contrast with standard weak strategies, we allow certain reductions to take place inside lambda-abstractions, which offers more sharing of redexes. We then present a generalized calculus where we can simulate arbitrary beta-reduction steps, and another weak calculus, which is a compromise between simplicity and generality. Our experimental results confirm that, for large combinator based terms, weak strategies based on these calculi out-perform standard evaluators. Moreover, we derive two abstract machines for strong reduction which inherit the efficiency of the weak evaluators.

A Rewriting Alternative to Reidemeister-Schrier
N. Ghani (University of Leicester, United Kingdom)
A. Heyworth (University of Leicester, United Kingdom)

One problem in computational group theory is to find a presentation of the subgroup generated by a set of elements of a group. The Reidermeister-Schreier algorithm was developed in the 1930's and gives a solution based upon enumerative techniques. This however means the algorithm can only be applied to finite groups. This paper proposes a rewriting based alternative to the Reidermeister-Schreier algorithm which has the advantage of being applicable to infinite groups.

On the complexity of higher-order matching in the linear lambda-calculus
S. Salvati (INPL, Vandoeuvre-lès-Nancy, France)
P. de Groote (INRIA, Vandoeuvre-lès-Nancy, France)

We prove that second-order matching in the linear $\lambda$-calculus with linear occurrences of the unknowns is NP-complete. This result shows that context matching and second-order matching in the linear $\lambda$-calculus are, in fact, two different problems.

Testing Extended Regular Language Membership Incrementally by Rewriting
G. Rosu (University of Illinois at Urbana-Champaign, Urbana, USA)
M. Viswanathan (University of Illinois at Urbana-Champaign, Urbana, USA)

In this paper we present lower bounds and rewriting algorithms for testing membership of a word to a regular language described by an extended regular expression. Motivated by intuitions from monitoring and testing, where the words to be tested (execution traces) are typically much longer than the size of the regular expressions (patterns or requirements), and by the fact that in many applications the traces are only available incrementally, on an event by event basis, our algorithms are based on an event-consumption idea: a just arrived event is consumed'' by the regular expression, i.e., the regular expression modifies itself into another expression discarding the event. We present an exponential space lower bound for monitoring extended regular expressions and argue that the presented rewriting-based algorithms, besides their simplicity and elegance, are practical and almost as good as one can hope. We experimented with and evaluated our algorithms in Maude.

Relating derivation lengths with the slow growing hierarchy directly
G. Moser (University of Münster, Germany)
A. Weiermann (University of Münster, Germany)

In this article we introduce the notion of a generalized system of fundamental sequences and we define its associated slow growing hierarchy. We claim that these concepts provide a bridge connecting (ordinal) proof theory and term rewriting theory. More precisely these concepts are genuinely related to the classification of the complexity---the derivation length--- of rewrite systems for which termination is proved by a standard termination ordering. To substantiate this claim, we re-obtain multiple recursive bounds on the the derivation length for rewrite systems terminating under lexicographic path ordering. The novelty of our proof being that is clarifies precisely the proof-theoretic concepts exploited in the original proof by the second author. In particular it reveals the role played by the slow-growing hierarchy.

Stable Computational Semantics of Conflict-free Rewrite Systems (Partial Orders with Duplication)
Z. Khasidashvili (Intel, Haifa, Israel)
J. Glauert (University Plain, Norwich, United Kingdom)

We study orderings on reductions in the style of Levy reflecting the growth of information w.r.t. (super)stable sets S of 'values' (such as head-normal forms or Bohm-trees). We show that sets of co-initial reductions ordered by such orderings form finitary w-algebraic complete lattices, i.e., form computation and Scott domains. As a consequence, we obtain a relativized version of computational semantics as proposed by Boudol for term rewriting systems. Furthermore, we give a pure domain-theoretic characterization of the orderings in the spirit of Kahn and Plotkin's concrete domains. These constructions are carried out in the framework of Stable Deterministic Residual Structures, which are abstract reduction systems with an axiomatized residual relations on redexes, and model all orthogonal (or conflict-free) reduction systems as well as many other interesting computation structures.

Residuals in Higher-Order Rewriting
S. Bruggink (University of Utrecht, The Netherlands)

An interesting topic of research within rewriting theory is residual theory: what remains of a reduction phi after another reduction psi, which starts at the same object, has been performed? The residual of phi after psi, written varphi/psi, should consist of exactly those steps of varphi, which were not performed by psi. Residuals were studied by Levy, Huet, Mellies, Van Oostrom & De Vrijer, and residual systems are defined. We mention the following important result: if a residual system can be specified for some rewriting system R then R is confluent. In this article we study residuals in Pattern Rewriting Systems, a subclass of Nipkow's Higher-Order Rewriting Systems (HRSs). First, the rewrite relation is defined by means of a higher-order rewriting logic, and proof terms in the style of Hilken are defined, which witness reductions. Now, we have the formal machinery to define a residual operator for PRSs, and we will prove the following theorem: Theorem: If H is an orthogonal HRS, then H with projection operator is a residual system. As a side-effect, all results of residual theory are inherited by orthogonal PRSs, such as confluence, and the notion of equivalence of reductions, also known as Levy- or permutation equivalence.

Confluence as a cut elimination property
G. Dowek (École polytechnique, Palaiseau, France)

The goal of this paper is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system: asymmetric deduction modulo this rewrite system and that the confluence property of the rewrite system is equivalent to the cut elimination property of the associated logical system. This equivalence, however, does not extend to rewrite systems on propositions.

Two-Way Equational Tree Automata for AC-like Theories: Decidability and Closure Properties
K.N. Verma (ENS Cachan, France)

We study two-way tree automata modulo equational theories. We deal with the theories of Abelian groups ($ACUM$), idempotent commutative monoids ($ACUI$), and the theory of exclusive-or ($ACUX$), as well as some variants including the theory of commutative monoids ($ACU$). We show that the one-way automata for all these theories are closed under union and intersection, and emptiness is decidable. For two-way automata the situation is more complex. In all these theories except $ACUI$, we show that two-way automata can be effectively reduced to one-way automata, provided some care is taken in the definition of the so-called push clauses. (The $ACUI$ case is open.) In particular, the two-way automata modulo these theories are closed under union and intersection, and emptiness is decidable. We also note that alternating variants have undecidable emptiness problem for most theories, contrarily to the non-equational case where alternation is essentially harmless.

Size-Change Termination for Term Rewriting
R. Thiemann (RWTH Aachen, Germany)
J. Giesl (RWTH Aachen, Germany)

In [Lee, Jones & Ben-Amram, 2001], a new size-change principle was proposed to verify termination of functional programs automatically. We extend this principle in order to prove termination and innermost termination of arbitrary term rewrite systems (TRSs). Moreover, we compare this approach with existing techniques for termination analysis of TRSs (such as recursive path orderings or dependency pairs). It turns out that the size-change principle on its own fails for many examples that can be handled by standard techniques for rewriting, but there are also TRSs where it succeeds whereas existing rewriting techniques fail. In order to benefit from their respective advantages, we show how to combine the size-change principle with classical orderings and with dependency pairs. In this way, we obtain a new approach for automated termination proofs of TRSs which is more powerful than previous approaches.

Expression Reduction Systems with Patterns
J. Forest (Université Paris-Sud, Orsay, France)
D. Kesner (Université Paris 7, Paris, France)

We introduce a new higher-order rewriting formalism, called Expression Reduction Systems with Patterns (ERSP), where abstraction is not only allowed on variables but also on nested patterns. These patterns are built by combining standard algebraic patterns with choice constructors used to denote different possible structures allowed for an abstracted argument. In other words, the non deterministic choice between different rewriting rules which is inherent to classical rewriting formalisms can be lifted here to the level of patterns. We show that confluence holds for a reasonable class of systems and terms.

Diagrams for Meaning Preservation
J.B. Wells (Heriot-Watt University, Edinburgh, United Kingdom)
D. Plump (University of York, United Kingdom)
F. Kamareddine (Heriot-Watt University, Edinburgh, United Kingdom)

This paper presents an abstract framework and multiple diagram-based methods for proving meaning preservation, i.e., that all rewrite steps of a rewriting system preserve the meaning given by an operational semantics based on a rewriting strategy. While previous rewriting-based methods have generally needed the treated rewriting system as a whole to have such properties as, e.g., confluence, standardization, and/or termination or boundedness of developments, our methods can work when all of these conditions fail, and thus can handle more rewriting systems. We isolate the new lift/project diagram as the key proof idea and show that previous rewriting-based methods (Plotkin's method based on confluence and standardization and Machkasova and Turbak's method) implicitly use this diagram. Furthermore, our framework and proof methods help reduce the proof burden substantially by, e.g., supporting separate treatment of partitions of the rewrite steps, needing only elementary diagrams for rewrite step interactions, excluding many rewrite step interactions from consideration, needing weaker termination properties, and providing generic support for using developments in combination with any method.

Monotonic AC-compatible semantic path orderings
C. Borralleras (Universitat de Vic, Spain)
A. Rubio (Universitat Politecnica de Catalunya, Barcelona, Spain)

Polynomial interpretations and RPO-like orderings allow one to prove termination of Associative and Commutative (AC-)rewriting by only checking the rules of the given rewrite system without considering the so-called extended rules. However, these methods have important limitations as termination proving tools. To overcome these limitations, more powerful methods like the dependency pairs method have been extended to the AC-case. Unfortunately, in order to ensure AC-termination, the extended rules, which, in general, are hard to prove, must be added to the rewrite system. In this paper we present a new automatable ordering-based termination proving method for AC-rewriting which does not need to consider extended rules. Due to this, we can easily prove several non-trivial examples appearing in the literature that, to our knowledge, can be handled by no other automatic method.

"Term Partition" for Mathematical Induction
P. Urso (Université de Nice - Sophia Antipolis, Nice, France)
E. Kounalis (Université de Nice - Sophia Antipolis, Nice, France)

A key new concept, term partition, allows to design a new method for proving theorems whose proof usually requires mathematical induction. A term partition of a term t is a well-defined splitting of t into a pair (a,b) of terms that describes the language of normal forms of the ground instances of t. If A is a monomorphic set of axioms (rules) and (a,b) is a term partition of t, then the normal form (obtained by using A) of any ground instance of t can be `divided'' into the normal forms (obtained by using A) of the corresponding ground instances of a and b. Given a conjecture t = s to be checked for inductive validity in the theory of A, a partition (a,b) of t and a partition (c,d) of s is computed. If a = c and b = d, then t = s is an inductive theorem for A. The method is conceptually different to the classical theorem proving approaches since it tries to directly mechanize the omega-rule. It allows to obtain elegant and natural proofs of a large number of conjectures (including non-linear ones) without additional lemmas and/or generalizations.

A Rule-Based Approach for Automated Generation of Kinetic Chemical Mechanisms
O. Bournez (LORIA & INRIA, Villers-lés-Nancy, France)
G.-M. Come (INPL-ENSIC, Nancy, France)
V. Conraud (LORIA & INRIA, Villers-lés-Nancy, France)
H. Kirchner (LORIA & INRIA, Villers-lés-Nancy, France)
L. Ibanescu (LORIA, Villers-lés-Nancy, France)

Several software systems have been developed recently for the automated generation of combustion reactions kinetic mechanisms using different representations of species and reactions and different generation algorithms. In parallel, several software systems based on rewriting have been developed for the easy modeling and prototyping of systems using rules controlled by strategies. This paper presents our current experience in using the rewrite system ELAN for the automated generation of the combustion reactions mechanisms previously implemented in the EXGAS kinetic mechanism generator system. We emphasize the benefits of using rewriting and rule-based programming controlled by strategies for the generation of kinetic mechanisms.

An E-unification algorithm for analyzing protocols that use modular exponentiation
D. Kapur (University of New Mexico, Albuquerque, USA)
P. Narendran (SUNY at Albany, USA)
L. Wang (SUNY at Albany, USA)

Multiplication and exponentiation modulo a prime are common operations in modern cryptography. Unification problems modulo some equational theories that these operations satisfy are investigated. The algorithms for some of these unification problems are expected to be integrated into Naval Research Lab.'s Protocol Analyzer (NPA), a tool developed by Catherine Meadows, which has been successfully used to analyze cryptographic protocols, particularly emerging standards such as the Internet Engineering Task Force's (IETF) Internet Key Exchange~\cite{ike} and Group Domain of Interpretation~\cite{gdoi} protocols. Currently, for equational unification, NPA uses narrowing procedures which work only for terminating and confluent rewrite systems. Given that modular multiplication is associative and commutative, NPA cannot be effectively applied for protocols that use these operations. Two different but related equational theories are analyzed here. A unification algorithm is given for one of the theories which relies on solving syzygies over multivariate integral polynomials with noncommuting indeterminates. For the other theory, in which the distributivity property of exponentiation over multiplication is assumed, the unifiability problem is shown to be undecidable by adapting a construction developed by one of the authors to reduce Hilbert's 10th problem to the solvability problem for linear equations over semi-rings. A new algorithm for computing strong \Groebner\ basis of right ideals over the polynomial ring Z is proposed; unlike earlier algorithms proposed by Baader as well as by Madlener and Reinert which work only for right admissible term orderings with the boundedness property, this algorithm works for {\em any\/} right admissible term ordering. Techniques from several different fields -- particularly symbolic computation (ideal theory and Groebner basis algorithms) and unification theory --- are used to address problems arising in state-based cryptographic protocol analysis.

ABSTRACTS OF SYSTEM DESCRIPTIONS

The Equational Prover of THEOREMA
T. Kutsia (SUNY at Albany, USA)

The paper describes the equational prover of Theorema. It is a prover for unit equational deduction implemented on Mathematica. The prover accepts input either in the first order or in the applicative higher order form. Besides, sequence variables can occur and a (restricted) usage of Mathematica built-in functions are allowed. Main proving method is unfailing completion, extended for terms with sequence variables, and narrowing (for existential goals). Mathematica technology is exploited to implement rewriting. Warren's translation method is used to transform applicative higher order expressions into the first order form. Proof presentation is based on a slightly modified variant of Equational Chain calculus. Implementation issues are discussed.

Tsukuba Termination Tool
N. Hirokawa (University of Tsukuba, Japan)
A. Middeldorp (University of Tsukuba, Japan)

We present a tool for automatically proving termination of first-order rewrite systems. The tool is based on the dependency pair method of Arts and Giesl. It incorporates several new techniques to make the method more efficient. The tool produces high-quality output and has a convenient web interface. We explain the features of the tool and we give some implementation details. We conclude with some experiments, including a brief comparison with other termination tools that implement the dependency pair method.

Rule-based Analysis of Dimensional Safety
F. Chen (University of Illinois at Urbana-Champaign, Urbana, USA)
G. Rosu (University of Illinois at Urbana-Champaign, Urbana, USA)
R.P. Venkatesan (University of Illinois at Urbana-Champaign, Urbana, USA)

Dimensional safety policy checking is an old topic in software analysis concerned with ensuring that programs do not violate basic principles of units of measurement. Scientific and/or navigation software is routinely dimensional and violations of measurement unit safety policies can hide significant domain-specific errors which are hard or impossible to find otherwise. Dimensional analysis of programs written in conventional programming languages is addressed in this paper. We draw general design principles for dimensional analysis tools and then discuss our prototypes, implemented by rewriting, which include both dynamic and static checkers. Our approach is based on assume/assert annotations of code which are properly interpreted by our tools and ignored by standard programming language compilers/interpreters. The output of our prototypes consists of warnings that list those expressions violating the unit safety policy. These prototypes are implemented in the rewriting system Maude, using more than 2,000 rewriting rules. This paper presents a non-trivial application of rewriting techniques to software analysis.

M. van den Brand (CWI, Amsterdam, The Netherlands and LORIA-INRIA, Villers-lés-Nancy, France)
P.-E. Moreau (LORIA-INRIA, Villers-lés-Nancy, France)
J. Vinju (CWI, Amsterdam, The Netherlands)

Term rewriting can only be applied if practical implementations of term rewriting engines exist. New rewriting engines are designed and implemented either to experiment with new (theoretical) results or to be able to tackle new application areas. In this paper we present the Meta-Environment: an environment rapidly implementing the syntax and semantics of term rewriting based formalisms. We provide not only the basic building blocks, but complete interactive programming environments that only need to be instantiated by the details of a new formalism.

Rewriting UNITY
A. Granicz (California Institute of Technology, Pasadena, USA)
D. Zimmerman (California Institute of Technology, Pasadena, USA)
J. Hickey (California Institute of Technology, Pasadena, USA)

In this paper we describe the implementation of the UNITY formalism as an extension of general-purpose languages and show its translation to C abstract syntax using Phobos, our generic front-end in the Mojave compiler. Phobos uses term rewriting to define the syntax and semantics of arbitrary languages, and automates their translation to an internal compiler representation. Furthermore, it provides access to formal reasoning capabilities using the integrated MetaPRL theorem prover, through which advanced optimizations and transformations can be implemented or formal proofs derived.

The Maude 2.0 System