Participant Support Costs for CI-EN: Collaborative: Run Your Research with Redex

Programming language researchers deal with models of programming languages, e.g., models of dynamic semantics, type systems, compilation strategies, static analysis tools, etc. With models, researchers validate new designs and communicate their essence to colleagues. To communicate properties of new designs, researchers formulate claims about these models and, after some testing, turn them into theorems. On some occasions, researchers also use models to explore the correctness of existing programming languages and systems. Over the past decade, the PI and his graduate students have built Redex, a framework in support of this activity, dubbed “semantics engineering.” In the past five or six years, Redex has escaped the PI’s lab and has been used by a constantly increasing number of people. It has supported the work in 10 dissertations (8 of which have been defended and 2 that are expected this year or early next year). It has been used for a number of large specification efforts, including Fortress, Guha’s JavaScript model (�JS), and the latest Scheme standard (R6RS). The original plan for the design of Redex was to enable research on small models of programming languages, and indeed, the PI and others have exploited it to facilitate their own research for many years. As Redex has grown, however, larger and larger models are being built and they are enabling research in other, unexpected ways. For example, there is a Redex model of the Racket virtual machine’s bytecode that gives a detailed account of the low-level structure of a realistic Racket programs. Danny Yoo used that model to be able to build a Racket bytecode to JavaScript compiler, enabling him to run Racket programs in the browser. Last year, the PI and several colleagues conducted a case study for Redex. The case study (1) confirmed that all selected papers contained mistakes, both small and large, and (2) validated Redex’s utility. It also exposed numerous short-comings that this proposal aims to address.