Run your research: on the effectiveness of lightweight mechanization

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.

References

1. Andrea Arcuri and Lionel C. Briand. A practical guide for using statistical tests to assess randomized algorithms in software engineering. In Proc. Intl. Conf. Soft. Eng. , pp. 1--10, 2011.
2. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Wash- burn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: the POPLMark Challenge. In Proc. Intl. Conf. Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science volume 3603, pp. 50--65, 2005.
3. Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov. Korat: automated testing based on Java predicates. In Proc. Intl. Symp. Soft. Testing and Analysis, pp. 123--133, 2002.
4. Avik Chaudhuri. A concurrent ML library in Concurrent Haskell. In Proc. ACM Intl. Conf. Functional Programming, pp. 269--280, 2009.
5. James Cheney and Alberto Momigliano. Mechanized metatheory model- checking. In Proc. Intl. Conf. Principles and Practice of Declarative Programming, pp. 75--86, 2007.
6. James Cheney and Christian Urban. αProlog: a logic programming language with names, binding, and α-equivalence. In Proc. Intl. Conf. Logic Programming, Lecture Notes in Computer Science volume 3132, pp. 269--283, 2004.
7. Koen Claessen and John Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proc. ACM Intl. Conf. Functional Programming, pp. 268--279, 2000.
8. Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Martin-Oliet, Jose Meseguer, and Carolyn Talcott. Maude 2.0 system. In Proc. Intl. Conf. Rewriting Techniques and Applications, Lecture Notes in Computer Science volume 2706, pp. 76--87, 2003.
9. John Clements, Matthew Flatt, and Matthias Felleisen. Modeling an algebraic stepper. In Proc. Euro. Symp. Programming, pp. 320--334, 2001.
10. Thierry Despeyroux. Executable specification of static semantics. In Proc. Intl. Symp. Semantics of Data Types, Lecture Notes in Computer Science volume 173, pp. 215--233, 1984.
11. Thierry Despeyroux. Typol: a formalism to implement natural semantics. INRIA, Research Report No. 94, 1988.
12. Atze Dijkstra and S. Doaitse Swierstra. Ruler: programming Type rules. In Proc. Intl. Symp. Functional and Logic Programming, Lecture Notes in Computer Science volume 3945, pp. 30--46, 2006.
13. Matthew B. Dwyer, Suzette Person, and Sebastian G. Elbaum. Controlling factors in evaluating path-sensitive error detection techniques. In Proc. ACM Symp. Foundations of Soft. Eng., pp. 92--104, 2006.
14. Chucky Ellison and Grigore Rosu. An Executable Formal Semantics of C with Applications. University of Illinois, http://hdl.handle.net/2142/25816, 2011..

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

      • Semantics

• Theory of computation

  • Semantics and reasoning

    • Program semantics