SLE 2016 Keynote: Redex: Lightweight Semantics Engineering
Channel: SPLASH2016
Date: 2016-11-15

Redex is a programming language designed to support semantics engineers as they experiment with programming language models. To explore a model, an engineer writes down grammars, type systems, and operational semantics in a notation inspired by the programming languages literature. Redex breathes life into the model, building typing derivations, running example expressions, and using random generation to falsify claims about the model.