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