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 I

      2.13 Lab Abstracting Abstract Machines I

        Exercises

      2.14 Abstracting Abstract Machines II

      2.15 Lab Abstracting Abstract Machines II

        Exercises

    3 Extended Exercises

      3.1 Objects: Problem

      3.2 Objects: Solution

      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.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