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, Sam Tobin-Hochstadt, Robert Bruce Findler

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Scopus citations

Abstract

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)
Title of host publicationPOPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages285-296
Number of pages12
DOIs
StatePublished - Mar 12 2012
Event39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12 - Philadelphia, PA, United States
Duration: Jan 25 2012Jan 27 2012

Other

Other39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12
CountryUnited States
CityPhiladelphia, PA
Period1/25/121/27/12

Keywords

  • Lightweight semantics engineering

ASJC Scopus subject areas

  • Software

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

Cite this