Lem : Reusable engineering of real-world semantics
- Submitting institution
-
The University of Leicester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2395
- Type
- E - Conference contribution
- DOI
-
10.1145/2628136.2628143
- Title of conference / published proceedings
- ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming
- First page
- 175
- Volume
- 49
- Issue
- 9
- ISSN
- 0362-1340
- Open access status
- Out of scope for open access requirements
- Month of publication
- August
- Year of publication
- 2014
- URL
-
-
- Supplementary information
-
https://doi.org/10.1145/2628136.2628143
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
4
- Research group(s)
-
-
- Citation count
- 7
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper introduced the LEM tool, a successor to the popular Ott tool (awarded the 2017 SIGPLAN ICFP “most influential paper”). LEM has had a huge impact on the field of formal specification, having been used to formalize processor models (3 papers in POPL and PLDI), C semantics (PLDI, POPL and OOPSLA), memory consistency models (multiple POPL papers). It has been the foundation for influential projects like the CakeML verified compiler. The SibylFS filesystem specification (SOSP’15) used LEM, and recently there have been papers on the Ethereum blockchain virtual machine, and associated verification of smart contracts.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -