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

Project: Research project

Project Details

Description

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.
StatusFinished
Effective start/end date8/1/147/31/17

Funding

  • National Science Foundation (CNS-1405756 001)

Fingerprint

Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.