|
- iRho
- An implementation of an interpreter for iRho, an imperative version of the Rewriting-calculus, based on pattern-matching, pattern-abstractions, and side-effects. The implementation contains a parser and a call-by-value 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 rho-calculus of Cirstea, Faure and Kirchner which is a version of the rho-calculus 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 (big-step) but also one describing the successive applications of evaluation rules (small-step). - 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.
