More Web Proxy on the site http://driver.im/

research-article

Lem: reusable engineering of real-world semantics

Authors:

Dominic P. Mulligan,

Kathryn E. Gray,

Peter SewellAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 9

Pages 175 - 188

https://doi.org/10.1145/2692915.2628143

Published: 19 August 2014 Publication History

Abstract

Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of real-world processors, programming languages, protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation; their scale adds engineering issues akin to those of programming to the task of writing clear and usable mathematics. But language and tool support for specification is lacking. Proof assistants can be used but bring their own difficulties, and a model produced in one, perhaps requiring many person-years effort and maintained over an extended period, cannot be used by those familiar with another.

We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem design takes inspiration both from functional programming languages and from proof assistants, and Lem definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX and HTML for presentation. This requires a delicate balance of expressiveness, careful library design, and implementation of transformations - akin to compilation, but subject to the constraint of producing usable and human-readable code for each target. Lem's effectiveness is demonstrated by its use in practice.

References

[1]

A. Asperti, C. Sacerdoti Coen, E. Tassi, and S. Zacchiroli. User interaction with the Matita proof assistant. J. Autom. Reason., 2006.

Digital Library

[2]

L. Augustsson. Compiling pattern matching. In Functional Programming Languages and Computer Architecture, LNCS 201. 1985. ISBN 978-3-540-15975-9. 10.1007/3-540-15975-4_48. URL http://dx.doi.org/10.1007/3-540-15975-4_48.

Digital Library

[3]

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In Proc. POPL, 2011.

Digital Library

[4]

M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell. Clarifying and compiling C/C++ concurrency: from C++ 11 to POWER. In Proc. POPL, 2012.

Digital Library

[5]

S. Berghofer, L. Bulwahn, and F. Haftmann. Turning inductive into equational specifications. In Proc. TPHOLs, 2009.

Digital Library

[6]

S. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith, and K. Wansbrough. Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. In Proc. SIGCOMM, 2005.

Digital Library

[7]

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A trusted mechanised JavaScript specification. In Proc. POPL, 2014.

Digital Library

[8]

T. Coquand. An analysis of girard's paradox. In Logic in Computer Science, 1986.

[9]

C. Ellison and G. Rosu. An executable formal semantics of C with applications. In Proc. POPL, 2012.

Digital Library

[10]

A. C. J. Fox and M. O. Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proc. ITP, 2010.

Digital Library

[11]

S. Goel, W. A. H. Jr., and M. Kaufmann. Abstract Stobjs and their application to ISA modeling. In Proc. ACL2 Workshop, 2013.

[12]

M. J. C. Gordon, J. Reynolds, W. A. H. Jr., and M. Kaufmann. An integration of HOL and ACL2. In Proc. FMCAD, 2006.

Digital Library

[13]

J. Hurd. The OpenTheory standard theory library. In NASA Formal Methods, LNCS 6617, 2011.

Digital Library

[14]

C. Kaliszyk and A. Krauss. Scalable LCF-Style proof translation. In Proc. ITP, LNCS 7998, 2013.

Digital Library

[15]

C. Keller and B. Werner. Importing HOL Light into Coq. In Proc. ITP, LNCS 6172, 2010. ISBN 3-642-14051-3, 978-3-642-14051-8. 10.1007/978-3-642-14052-5_22. URL http://dx.doi.org/10.1007/978-3-642-14052-5_22.

Digital Library

[16]

C. Klein, J. Clements, C. Dimoulas, C. Eastlund, M. Felleisen, M. Flatt, J. A. McCarthy, J. Rafkind, S. Tobin-Hochstadt, and R. B. Findler. Run your research: on the effectiveness of lightweight mechanization. In Proc. POPL, 2012. ISBN 978-1-4503-1083-3.

Digital Library

[17]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an OS kernel. In Proc. SOSP, 2009.

Digital Library

[18]

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens. CakeML: A Verified Implementation of ML. In Proc. POPL, 2014.

Digital Library

[19]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43 (4): 363--446, 2009.

Digital Library

[20]

J. Lim and T. Reps. TSL: A system for generating abstract interpreters and its application to machine-code analysis. TOPLAS, 35 (1), 2013.

Digital Library

[21]

S. Mador-Haim, L. Maranget, S. Sarkar, K. Memarian, J. Alglave, S. Owens, R. Alur, M. M. K. Martin, P. Sewell, and D. Williams. An axiomatic memory model for POWER multiprocessors. In CAV, 2012.

Digital Library

[22]

L. Maranget. Compiling pattern matching to good decision trees. In Proc. Workshop on ML, 2008. ISBN 978-1-60558-062-3. 10.1145/1411304.1411311. URL http://doi.acm.org/10.1145/1411304.1411311.

Digital Library

[23]

J. Meseguer. Twenty years of rewriting logic. In Proc. WRLA, WRLA'10, 2010.

Digital Library

[24]

G. Morrisett, G. Tan, J. Tassarotti, J.-B. Tristan, and E. Gan. RockSalt: better, faster, stronger SFI for the x86. In Proc. PLDI, 2012.

Digital Library

[25]

S. Owens. A sound semantics for OCaml light. In Proc. ESOP, LNCS 4960, 2008.

Digital Library

[26]

S. Owens, P. Böhm, F. Zappa Nardelli, and P. Sewell. Lem: A lightweight tool for heavyweight semantics. In Proc. ITP, LNCS 6898, pages 363--369, 2011. "Rough Diamond" section.

Digital Library

[27]

J. G. Politz, M. J. Carroll, B. S. Lerner, J. Pombrio, and S. Krishnamurthi. A tested semantics for getters, setters, and eval in JavaScript. In Proc. DSL, 2012.

Digital Library

[28]

T. Rittweiler and F. Haftmann. Haskabelle - converting Haskell source files to Isabelle/HOL theories. http://isabelle.in.tum.de/haskabelle.html.

[29]

G. Roşu and T. F. Şerbănuţă. An overview of the K semantic framework. J. Logic and Algebraic Programming, 79 (6): 397--434, 2010.

[30]

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding POWER multiprocessors. In Proc. PLDI, 2011.

Digital Library

[31]

S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell, L. Maranget, J. Alglave, and D. Williams. Synchronising C/C++ and POWER. In Proc. PLDI, 2012.

Digital Library

[32]

Sewell, Sarkar, Owens, Zappa Nardelli, and Myreen}cacmP. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, and M. O. Myreen. x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors. C. ACM, 53 (7): 89--97, 2010.

Digital Library

[33]

P. Sewell, F. Zappa Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strni73353;a. Ott: Effective tool support for the working semanticist. J. Funct. Program., 20 (1): 71--122, 2010. ISSN 0956-7968.

Digital Library

[34]

M. Sozeau. Subset coercions in Coq. In TYPES, volume 4502 of Lecture Notes in Computer Science, pages 237--252, 2007.

Digital Library

[35]

M. G. J. van den Brand, A. Deursen, J. Heering, H. A. d. Jong, M. Jonge, T. Kuipers, P. Klint, L. Moonen, P. A. Olivier, J. Scheerder, J. J. Vinju, E. Visser, and J. Visser. The ASF+SDF meta-environment: A component-based language development environment. In Proc. LDTA, ENTCS 44, 2001.

[36]

J. Ševčík, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell. CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM, 60 (3): 22:1--22:50, June 2013. ISSN 0004-5411. 10.1145/2487241.2487248. URL http://doi.acm.org/10.1145/2487241.2487248.

Digital Library

[37]

D. Vytiniotis, S. L. P. Jones, T. Schrijvers, and M. Sulzmann. OutsideIn(X) modular type inference with local assumptions. J. Funct. Program., 21 (4-5): 333--412, 2011.

Digital Library

[38]

P. Wadler. Views: a way for pattern matching to cohabit with data abstraction. In Proc. POPL, 1987. ISBN 0-89791-215-2. 10.1145/41625.41653. URL http://doi.acm.org/10.1145/41625.41653.

Digital Library

[39]

F. Wiedijk. Encoding the HOL Light logic in Coq, 2007. Note.

[40]

J. Zhao, S. Nagarakatte, M. M. K. Martin, and S. Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In Proc. POPL, 2012.

Digital Library

Cited By

Khan ZNamin A(2024)A Survey of Vulnerability Detection Techniques by Smart Contract ToolsIEEE Access10.1109/ACCESS.2024.340162312(70870-70910)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3401623
Feng ZYongwang ZYang LJun S(2024)A Comprehensive Formal Specification of ARINC 653 With Conformity ProofSoftware Testing, Verification and Reliability10.1002/stvr.190135:1Online publication date: Oct-2024
https://doi.org/10.1002/stvr.1901
Albert EGenaim SKirchner DMartin-Martin E(2023)Formally Verified EVM Block-OptimizationsComputer Aided Verification10.1007/978-3-031-37709-9_9(176-189)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37709-9_9
Show More Cited By

Index Terms

Lem: reusable engineering of real-world semantics
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
  2. Software notations and tools
    1. System description languages
      1. Specification languages
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Lem: reusable engineering of real-world semantics
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of real-world processors, programming languages, protocols, and security mechanisms, for testing, proof, ...
Soundness and Completeness Proofs by Coinductive Methods

We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an ...
Psi-Calculi in Isabelle

This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 9

ICFP '14

September 2014

361 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2692915

Editors:
Mark W. Bailey
Hamilton College, Clinton, NY
,
Rajeev Balasubramonian
University of Utah
,
Al Davis
University of Utah
,
Sarita Adve
University of Illinois at Urbana-Champ

Issue’s Table of Contents

ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming
August 2014
390 pages
ISBN:9781450328739
DOI:10.1145/2628136
General Chair:
Johan Jeuring
Universiteit Utrecht, The Netherlands
,
Program Chair:
Manuel M.T. Chakravarty
University of New South Wales, Australia

Copyright © 2014 ACM.

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: 19 August 2014

Published in SIGPLAN Volume 49, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

77
Total Citations
View Citations
421
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)4

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Khan ZNamin A(2024)A Survey of Vulnerability Detection Techniques by Smart Contract ToolsIEEE Access10.1109/ACCESS.2024.340162312(70870-70910)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3401623
Feng ZYongwang ZYang LJun S(2024)A Comprehensive Formal Specification of ARINC 653 With Conformity ProofSoftware Testing, Verification and Reliability10.1002/stvr.190135:1Online publication date: Oct-2024
https://doi.org/10.1002/stvr.1901
Albert EGenaim SKirchner DMartin-Martin E(2023)Formally Verified EVM Block-OptimizationsComputer Aided Verification10.1007/978-3-031-37709-9_9(176-189)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37709-9_9
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
Alhabardi FLazar BSetzer A(2022)Verifying Correctness of Smart Contracts with Conditionals2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain & Beyond (iGETblockchain)10.1109/iGETblockchain56591.2022.10087054(1-6)Online publication date: 7-Nov-2022
https://doi.org/10.1109/iGETblockchain56591.2022.10087054
Marmsoler DBrucker A(2021)A Denotational Semantics of Solidity in Isabelle/HOLSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_23(403-422)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.1007/978-3-030-92124-8_23
Khan ZSiami Namin A(2020)Ethereum Smart Contracts: Vulnerabilities and their Classifications2020 IEEE International Conference on Big Data (Big Data)10.1109/BigData50022.2020.9439088(1-10)Online publication date: 10-Dec-2020
https://doi.org/10.1109/BigData50022.2020.9439088
Kant PHammond KCoutts DChapman JClarke NCorduan JDavies NDíaz JGüdemann MJeltsch WSzamotulski MVinogradova P(2020)Flexible Formality Practical Experience with Agile Formal MethodsTrends in Functional Programming10.1007/978-3-030-57761-2_5(94-120)Online publication date: 18-Aug-2020
https://doi.org/10.1007/978-3-030-57761-2_5
An XTahat ARavindran B(2020)A Validation Methodology for OCaml-to-PVS TranslationNASA Formal Methods10.1007/978-3-030-55754-6_12(207-221)Online publication date: 11-May-2020
https://dl.acm.org/doi/10.1007/978-3-030-55754-6_12
Banach R(2020)Verification-Led Smart ContractsFinancial Cryptography and Data Security10.1007/978-3-030-43725-1_9(106-121)Online publication date: 13-Mar-2020
https://doi.org/10.1007/978-3-030-43725-1_9
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.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents