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 manual consists of two parts: a tutorial introduction and a reference for Redex. Also see http://redex.racket-lang.org/ and the examples subdirectory in the redex collection.

    1 Amb: A Redex Tutorial

      1.1 Defining a Language

      1.2 Typing

      1.3 Testing Typing

      1.4 Defining a Reduction Relation

      1.5 Testing Reduction Relations

      1.6 Random Testing

      1.7 Typesetting the Reduction Relation

      1 Bibliography

    2 The Redex Reference

      2.1 Patterns

      2.2 Terms

      2.3 Languages

      2.4 Reduction Relations

      2.5 Other Relations

      2.6 Testing

      2.7 GUI

      2.8 Typesetting

        2.8.1 Picts, PDF, & PostScript

        2.8.2 Customization

        2.8.3 Removing the Pink Background