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

This the source for the Racket packages: "redex", "redex-benchmark", "redex-doc", "redex-examples", "redex-gui-lib", "redex-lib", "redex-pict-lib", "redex-test".

Contribute to Racket by submitting a pull request, reporting an issue, joining the development mailing list, or visiting the IRC or Slack channels.

Racket, including these packages, is free software, see LICENSE for more details.

By making a contribution, you are agreeing that your contribution is licensed under the Apache 2.0 license and the MIT license.