Racket has a DSL for describing programming language semantics called "PLT Redex", tutorial here: https://docs.racket-lang.org/redex/tutorial.html https://docs.

Racket has a DSL for describing programming language semantics called "PLT Redex", tutorial here: https://docs.racket-lang.org/redex/tutorial.html https://docs.racket-lang.org/redex/tutorial.html It has its own renderer, so you can take your code and render it for insertion into a paper. It uses Felleisen-style reduction syntax, which is useful because it exposes the current continuation of a program explicitly.