PLT Redex is a domain-specific language designed for specifying and debugging operational semantics. Write down a grammar and the reduction rules, and PLT Redex produces a stepper. It also provides support for building a test suites from the specification of a semantics.

PLT Redex is embedded in PLT Scheme, meaning all of the convenince of a modern programming language is available, including standard libraries (and non-standard ones) and a program-development environment.

Getting started: Install PLT Scheme, start up DrScheme, set your language to the “Module” language, and start your program with this:

Documentation: The reference manual contains all of the gory details of all of Redex's operators.

Scholarly paper: A paper on an early version of PLT Redex appeared at the International Conference on Rewriting Techniques and Applications (RTA) in 2004. Beware: the notations are different now (and there were fewer features back then).