research-article

Run your research: on the effectiveness of lightweight mechanization

Authors:

Robert Bruce FindlerAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 1

Pages 285 - 296

https://doi.org/10.1145/2103621.2103691

Published: 25 January 2012 Publication History

Get Access

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.

Supplementary Material

JPG File (popl_4b_3.jpg)

Download
21.37 KB

ZIP File (popl180.zip)

This directory accompanies the paper: Run Your Research: On the Effectiveness of Lightweight Mechanization_ by Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler It contains the models that we used when testing the papers from ICFP 2009. The README in the archive has more information.

Download
1.83 MB

MP4 File (popl_4b_3.mp4)

Download
278.67 MB

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.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[4]

Avik Chaudhuri. A concurrent ML library in Concurrent Haskell. In Proc. ACM Intl. Conf. Functional Programming, pp. 269--280, 2009.

Digital Library

Google Scholar

[5]

James Cheney and Alberto Momigliano. Mechanized metatheory model- checking. In Proc. Intl. Conf. Principles and Practice of Declarative Programming, pp. 75--86, 2007.

Digital Library

Google Scholar

[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.

Google Scholar

[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.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[9]

John Clements, Matthew Flatt, and Matthias Felleisen. Modeling an algebraic stepper. In Proc. Euro. Symp. Programming, pp. 320--334, 2001.

Digital Library

Google Scholar

[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.

Google Scholar

[11]

Thierry Despeyroux. Typol: a formalism to implement natural semantics. INRIA, Research Report No. 94, 1988.

Google Scholar

[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.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[14]

Chucky Ellison and Grigore Rosu. An Executable Formal Semantics of C with Applications. University of Illinois, http://hdl.handle.net/2142/25816, 2011.

Google Scholar

Cited By

View all

Ghica DLindley SBravo MPiróg M(2022)High-level effect handlers in C++Proceedings of the ACM on Programming Languages10.1145/35634456:OOPSLA2(1639-1667)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563445
Koppel JKearl JSolar-Lezama A(2022)Automatically deriving control-flow graph generators from operational semanticsProceedings of the ACM on Programming Languages10.1145/35476486:ICFP(742-771)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547648
Gurdeep Singh RScholliers C(2021)GraphRedex: Look at your researchSoftware: Practice and Experience10.1002/spe.295951:6(1322-1351)Online publication date: 3-Mar-2021
https://doi.org/10.1002/spe.2959
Show More Cited By

Index Terms

Run your research: on the effectiveness of lightweight mechanization
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Run your research: on the effectiveness of lightweight mechanization
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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, ...
The Intel labs Haskell research compiler
Haskell '13

The Glasgow Haskell Compiler (GHC) is a well supported optimizing compiler for the Haskell programming language, along with its own extensions to the language and libraries. Haskell's lazy semantics imposes a runtime model which is in general difficult ...
The Implementation of Run-Time Diagnostics in Pascal

This paper considers the role of run-time diagnostic checking in enforcing the rules of the Pascal programming language. Run-time diagnostic checks must be both complete (covering all language requirements) and efficient. Further, such checks should be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 47, Issue 1

POPL '12

January 2012

569 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2103621

Issue’s Table of Contents

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2012
602 pages
ISBN:9781450310833
DOI:10.1145/2103656
General Chair:
John Field
Google, USA
,
Program Chair:
Michael Hicks
University of Maryland, College Park, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2012

Published in SIGPLAN Volume 47, Issue 1

Check for updates

Author Tag

lightweight semantics engineering

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

70
Total Citations
View Citations
813
Total Downloads

Downloads (Last 12 months)34
Downloads (Last 6 weeks)7

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ghica DLindley SBravo MPiróg M(2022)High-level effect handlers in C++Proceedings of the ACM on Programming Languages10.1145/35634456:OOPSLA2(1639-1667)Online publication date: 31-Oct-2022
Koppel JKearl JSolar-Lezama A(2022)Automatically deriving control-flow graph generators from operational semanticsProceedings of the ACM on Programming Languages10.1145/35476486:ICFP(742-771)Online publication date: 31-Aug-2022
Gurdeep Singh RScholliers C(2021)GraphRedex: Look at your researchSoftware: Practice and Experience10.1002/spe.295951:6(1322-1351)Online publication date: 3-Mar-2021
Dabral CMartens CLelis LThue D(2020)Generating explorable narrative spaces with answer set programmingProceedings of the Sixteenth AAAI Conference on Artificial Intelligence and Interactive Digital Entertainment10.5555/3505464.3505471(45-51)Online publication date: 19-Oct-2020
Ofenbeck GRompf TPüschel MBiboudis AJonnalagedda MStucki SUreche V(2016)RandIR: differential testing for embedded compilersProceedings of the 2016 7th ACM SIGPLAN Symposium on Scala10.1145/2998392.2998397(21-30)Online publication date: 30-Oct-2016
Biboudis AJonnalagedda MStucki SUreche V(2016)Proceedings of the 2016 7th ACM SIGPLAN Symposium on ScalaundefinedOnline publication date: 30-Oct-2016
Churchill MMosses PSculthorpe NTorrini P(2015)Reusable Components of Semantic SpecificationsTransactions on Aspect-Oriented Software Development XII10.1007/978-3-662-46734-3_4(132-179)Online publication date: 20-Mar-2015
Filaretti DMaffeis S(2014)An Executable Formal Semantics of PHPProceedings of the 28th European Conference on ECOOP 2014 --- Object-Oriented Programming - Volume 858610.1007/978-3-662-44202-9_23(567-592)Online publication date: 1-Aug-2014
Mosses PNaik MPereira FTitzer B(2024)Towards Verification of a Denotational Semantics of InheritanceProceedings of the Workshop Dedicated to Jens Palsberg on the Occasion of His 60th Birthday10.1145/3694848.3694852(5-13)Online publication date: 22-Oct-2024
Bowman W(2024)A Low-Level Look at A-Normal FormProceedings of the ACM on Programming Languages10.1145/36897178:OOPSLA2(165-191)Online publication date: 8-Oct-2024
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Run your research: on the effectiveness of lightweight mechanization

The Intel labs Haskell research compiler

The Implementation of Run-Time Diagnostics in Pascal