On this page:
Redex:   Practical Semantics Engineering

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


    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

        2.8.4 LWs

      2.9 Macros and Typesetting

    3 Automated Testing Benchmark

      3.1 Managing Benchmark Modules

      3.2 Running Benchmark Models

      3.3 Logging

      3.4 Plotting

      3.5 Benchmark Models