Run your research: On the effectiveness of lightweight mechanization

Casey Klein*, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Tobin Hochstadt Sam, Robert Bruce Findler

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

43 Scopus citations


Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language tool; or the essence of a program analysis. No matter which role it plays, however, a faulty model doesn't serve its purpose. One way to eliminate flaws from a model is to write it down in a mechanized formal language. It is then possible to state theorems about the model, to prove them, and to check the proofs. Over the past nine years, PLT has developed and explored a lightweight version of this approach, dubbed Redex. In a nutshell, Redex is a domain-specific language for semantic models that is embedded in the Racket programming language. The effort of creating a model in Redex is often no more burdensome than typesetting it with LaTeX; the difference is that Redex comes with tools for the semantics engineering life cycle. In this paper we report on a validation of this form of lightweight mechanization. The largest part of this validation concerns the formalization and exploration of nine ICFP 2009 papers in Redex, an effort that uncovered mistakes in all nine papers. The results suggest that Redex-based lightweight modeling is effective and easy to integrate into the work flow of a semantics engineer. This experience also suggests lessons for the developers of other mechanization tools.

Original languageEnglish (US)
Pages (from-to)285-296
Number of pages12
JournalACM SIGPLAN Notices
Issue number1
StatePublished - Jan 1 2012


  • Lightweight semantics engineering

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Run your research: On the effectiveness of lightweight mechanization'. Together they form a unique fingerprint.

Cite this