On this page:
Redex:   Practical Semantics Engineering
8.15.0.2

Redex: Practical Semantics Engineering🔗ℹ

Robert Bruce Findler,
Casey Klein,
Burke Fetscher,
and Matthias Felleisen

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 four parts: a short tutorial introduction, a long tutorial introduction, a reference manual for Redex, and a description of the Redex automated testing benchmark suite. 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 Long Tutorial

      2.1 The Theoretical Framework

      2.2 Syntax and Metafunctions

        2.2.1 Developing a Language

        2.2.2 Developing Metafunctions

        2.2.3 Developing a Language 2

        2.2.4 Extending a Language: any

        2.2.5 Substitution

      2.3 Lab Designing Metafunctions

        Exercises

      2.4 Reductions and Semantics

        2.4.1 Contexts, Values

        2.4.2 Reduction Relations

        2.4.3 Semantics

        2.4.4 What are Models

      2.5 Lab Designing Reductions

        Exercises

      2.6 Types and Property Testing

        2.6.1 Types

        2.6.2 Developing Type Judgments

        2.6.3 Subjection Reduction

      2.7 Lab Type Checking

        Exercises

      2.8 Imperative Extensions

        2.8.1 Variable Assignment

        2.8.2 Raising Exceptions

      2.9 Lab Contexts and Stores

        Exercises

      2.10 Abstract Machines

        2.10.1 CC Machine

        2.10.2 The CK Machine

        2.10.3 The CC-CK Theorem

        2.10.4 The CEK machine

        2.10.5 The CEK-CK Theorem

      2.11 Lab Machine Transitions

        Exercises

      2.12 Abstracting Abstract Machines

      2.13 "common.rkt"

      2.14 "close.rkt"

      2.15 "tc-common.rkt"

      2.16 "extend-lookup.rkt"

    3 Extended Exercises

      3.1 Problem: Objects

      3.2 Solution: Objects

      3.3 Problem: Types

      3.4 Solution: Types

      3.5 Problem: Missionaries and Cannibals

      3.6 Solution: Missionaries and Cannibals

      3.7 Problem: Towers of Hanoi

      3.8 Solution: Towers of Hanoi

      3.9 Problem: GC

      3.10 Solution: GC

      3.11 Problem: Finite State Machines

      3.12 Solution: Finite State Machines

      3.13 Problem: Threads

      3.14 Solution: Threads

      3.15 Problem: Contracts

      3.16 Solution: Contracts

      3.17 Problem: Binary Addition

      3.18 Solution: Binary Addition

    4 The Redex Reference

      4.1 Patterns

      4.2 Terms

      4.3 Languages

        4.3.1 Binding Forms

        4.3.2 Multiple Variables in a Single Scope

        4.3.3 Ellipses in Binding Forms

        4.3.4 Compound Forms with Binders

        4.3.5 Binding Repetitions

      4.4 Reduction Relations

      4.5 Other Relations

      4.6 Testing

      4.7 GUI

      4.8 Typesetting

        4.8.1 Picts, PDF, & PostScript

        4.8.2 Customization

        4.8.3 Removing the Pink Background

        4.8.4 LWs

        4.8.5 Macros and Typesetting

    5 Automated Testing Benchmark

      5.1 The Benchmark Models

        5.1.1 stlc

        5.1.2 poly-stlc

        5.1.3 stlc-sub

        5.1.4 let-poly

        5.1.5 list-machine

        5.1.6 rbtrees

        5.1.7 delim-cont

        5.1.8 rvm

      5.2 Managing Benchmark Modules

      5.3 Running Benchmark Models

      5.4 Logging

      5.5 Plotting

      5.6 Finding the Benchmark Models

    Bibliography

    Index