PLT Redex is a domain-specific language and a collection of tools in Racket that are used to create executable specifications of programming languages. From descriptions of operational semantics and typing rules, Redex can both generate interpreters and type checkers and provide QuickCheck-style random inputs to them. With some customization, it can also generate figures for papers. We'll walk through a Redex model of a small DSL.
But a language is more than its type system and operational semantics. Domain-specific languages should be usable by domain experts, but domain experts are rarely comfortable with parentheses and they do not readily admit axiomatization. By using some of Racket's extensibility features, a model in Redex can be provided with a realistic concrete syntax and a development environment in DrRacket. I'll also show you how to do this.
No specific Racket background will be presumed, but basic familiarity with operational semantics and type systems will be helpful for the middle part of the demo.
David Thrane Christiansen is a Senior Software Developer at Deon Digital, where he works on developer experience for a declarative DSL for specifying commercial contracts. Together with Dan Friedman, he wrote The Little Typer, an introduction to dependent type theory. He has also contributed to the Idris language.
We have set up a collaboration with Prosa, who generously offered to provide a location for our regular meetups. Please see Prosa's Calendar for more details: Prosa Calendar (https://www.prosa.dk/kalender/hele-kalenderen/)
The ADA meeting room fits about 25 people and if we need more space, we can use the canteen (PASCAL), which has a capacity of at most 50 (fire regulation).
Ramón and Joakim