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 allows you to interactively explore terms and to use randomized test generation to attempt to falsify properties of your semantics.
PLT Redex is embedded in Racket, meaning all of the convenience of a modern programming language is available, including standard libraries (and non-standard ones) and a program-development environment.
Getting started: Install Racket, start up DrRacket, and start your program with this:
Book: Semantics Engineering with PLT Redex (SEwPR) by Matthias Felleisen, Robby Findler, and Matthew Flatt gives the mathematical background for operational semantics, as well as a tutorial introduction to Redex. The preface, table of contents, and an example syllabus are available online. The book is available from MIT Press.
Documentation: The reference manual contains all of the gory details of all of Redex's operators.
Citation: If you use a reduction semantics and/or you modeled a reduction semantics with Redex and you wish to give academic credit, please cite the book (above). If you are studying the effectiveness of meta-tools, the proper citation is our POPL 2012 paper.