
 iRho
 An implementation of an interpreter for iRho, an imperative version of the Rewritingcalculus, based on patternmatching, patternabstractions, and sideeffects. The implementation contains a parser and a callbyvalue evaluator in Natural Semantics; everything is written using the programming language Scheme. The core of this implementation (evaluator) is certified using the proof assistant Coq. Performances are honest compared to the minimal essence of the implementation. The final objective of this implementation is to make iRho a, so called, "agile programming language", in the vein of some useful scripts languages, like, e.g. Python and Ruby, where proof search is not only feasible but easy.
 xRho
 An implementation in the language Tom of the explicit rhocalculus of Cirstea, Faure and Kirchner which is a version of the rhocalculus with explicit handling of matching and substitution. The implementation is suprisingly short (few lines) and close to the operational semantics of the calculus taking advantage of all the capabilites of Tom.
The interpreter provides several evaluation modes including one giving directly the normal form (bigstep) but also one describing the successive applications of evaluation rules (smallstep).  ELAN
 Environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. It offers a natural and simple logical framework for the combination of the computation and deduction paradigms as it is backed up by the concepts of rewriting calculus and rewriting logic. It permits to support the design of theorem provers, logic programming languages, constraint solvers and decision procedures and to offer a modular framework for studying their combination.
 Rogue
 An imperative rewriting language that extends an untyped version of the Rewriting Calculus with mutable expression attributes. (Micro)Rogue is based on explicit binding and dynamic rules and microcode for rewriting.