Version: 5.0.2

Redex: Practical Semantics Engineering

Robert Bruce Findler
and Casey Klein

PLT Redex consists of a domain-specific language for specifying reduction semantics, plus a suite of tools for working with the semantics.

This is a reference manual for Redex. See for a gentler overview. (See also the examples subdirectory in the redex collection.)

To load Redex use:
which provides all of the names documented in this library.

The module redex/reduction-semantics provides only the non-GUI portions of what is described in this manual (everything except the last two sections), making it suitable for use with racket scripts.

    1 Patterns

    2 Terms

    3 Languages

    4 Reduction Relations

    5 Metafunctions and Relations

    6 Testing

    7 GUI

    8 Typesetting

      8.1 Picts & PostScript

      8.2 Customization

    9 Removing the pink background from PLT Redex rendered picts and ps files

      9.1 LW