Lightweight Semantics Engineering with Redex
summary
Redex is presented as a lightweight, Racket-embedded executable semantics DSL for rapid prototyping: write a grammar, reduction rules, judgment forms, then run an interpreter, trace steps, and generate paper-ready PDF snippets. The demo builds a call-by-value lambda calculus, implements both a manual subst and the built-in substitute binding forms, adds evaluation contexts, and uses redex-check to find counterexamples; random search finds counterexamples only after adding a closed-term judgment and restricted subsets, so the tools work but need scaffolding for disciplined results.
AI-written summary · about
chapters (8)
- 0:00Redex introduction
- 2:52Defining grammar
- 8:07Writing reduction rules
- 14:35Substitution and types
- 17:23Contexts for reductions
- 20:17Testing step reduction
- 22:46Random counterexamples
- 23:51Q&A
related talks
17mMacros for Domain-Specific Languages
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
45mLanguage-Oriented Programming with Racket
15mA Principled Approach to REPL Interpreters
01h 01mChallenges in the Design and Implementation of Teaching Languages for EDSLs
15mSulfur: Substitution Generation using a Logical Framework
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
32mExperience Report: Graph Rewriting with Lexical Effect Handlers