On this page:
Redex:   Practical Semantics Engineering
6.2

Redex: Practical Semantics Engineering

Robert Bruce Findler,
Casey Klein,
and Burke Fetscher

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 The Benchmark Models

        3.1.1 stlc

        3.1.2 poly-stlc

        3.1.3 stlc-sub

        3.1.4 let-poly

        3.1.5 list-machine

        3.1.6 rbtrees

        3.1.7 delim-cont

        3.1.8 rvm

      3.2 Managing Benchmark Modules

      3.3 Running Benchmark Models

      3.4 Logging

      3.5 Plotting

      3.6 Finding the Benchmark Models

    Bibliography

    Index