▼Experimenting with Languages in Redex
On this page:
Experimenting with Languages in Redex
8.3.0.10
    ← prev  up  next → 

Experimenting with Languages in Redex

William J. Bowman <wjb@williamjbowman.com>

In this tutorial, I introduce Redex the way I approach Redex: as a tool to explore and experiment with languages. I also explain some of my useful conventions and patterns, common problems I run into in Redex, and tricks to avoid problems as best I can.

This tutorial is aimed at programming languages researchers who understand programming languages formalism, but want to understand how to use Redex as an assistant in exploring formal models. I explain Redex in context, by example. I primarily focus on how I use it to work, and leave most details of Redex forms to the Redex documentation.

I will use the simply-typed λ-calculus with box modality as a running example, because I happen to be studying this calculus at the time of writing.

Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. 2001. https://doi.org/10.1017/s0960129501003322.

The source for this tutorial is online at https://github.com/wilbowma/experimenting-with-redex. Feel free to report issues, typos, etc there.

    1 Preface—Why Redex

    2 Syntax in Redex

      2.1 Syntax TLDR

      2.2 Defining Syntax

      2.3 Pattern Matching

      2.4 Extending Syntax and Syntax with Holes (Contexts)

      2.5 Binding, Substitution, and α-equivalence

      2.6 Random Generation of Syntax

      2.7 Testing Syntax

      2.8 Caveat: Syntax with Side Conditions

      2.9 Pitfall: All Symbols are Variables

      2.10 Pitfall: Subscripts and Unicode

    3 Reduction and Evaluation in Redex

      3.1 Reduction TLDR

      3.2 Small-step Reduction

      3.3 Evaluation and Normalization

      3.4 Testing Reduction Relations

      3.5 Caveat: Compatible Closure of Mutually Defined Relations

    4 Judgments in Redex

      4.1 Judgment TLDR

      4.2 βη-equality Judgment

      4.3 Typing Judgment

      4.4 Testing Judgments

      4.5 Meta-theory Random-testing

      4.6 Pitfall: Using the Wrong Language Name

      4.7 Caveat: Debugging Judgments

      4.8 Caveat: Ellipses and Racket Escapes

    ← prev  up  next →