Semantics Engineering with PLT Redex

By Matthias Felleisen, R. Findler, M. Flatt. 2009

338 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/f9831c5e97b7e14df93de6b87ff1285361b5b6dc

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

1. Emina Torlak
2. Shriram Krishnamurthi
3. Joe Gibbs Politz
4. Rastislav Bodík
5. Junsong Li
6. Alejandro Martinez
7. Sumner Warren
8. Mae Milano

Citations in the corpus

• A Tested Semantics for the Python Programming Language (2013, methodology): “• a core semantics for Python, dubbed λπ , which is defined as a reduction semantics using PLT Redex [3]; • an interpreter, dubbed λπ↓, implemented in 700LOC of Racket, that has been tested against the Redex model; • a desugaring translation from Python programs to λπ , implemented in Racket; • a de”
• CakeML: a verified implementation of ML (2014, unknown): “To precisely define divergence, and to support a syntactic type-soundness proof [31], we also give a small-step semantics for expressions as a CEK machine [5], and prove that it is equivalent to the big-step relation.”
• Growing solver-aided languages with rosette (2013, methodology): “Semantics Engineering with PLT Redex.”