Lem: reusable engineering of real-world semantics
- Submitting institution
-
The University of Kent
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 9334
- Type
- E - Conference contribution
- DOI
-
10.1145/2628136.2628143
- Title of conference / published proceedings
- Proceedings of the 19th ACM SIGPLAN international conference on Functional programming - ICFP '14
- 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
-
https://kar.kent.ac.uk/36713/
- Supplementary information
-
-
- 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
- Key interfaces in hardware and software systems need to be given precise specifications so that they can be tested and rigorously reasoned about. This paper is significant because it describes the Lem tool which introduces a new language for expressing semantic definitions. Its backend provides automatic output of definitions in Coq, HOL4, Isabelle/HOL, executable OCaml and Latex. Lem underpins a large amount of research on the REMS programme grant (EP/K008528/1, £5.6M) between Cambridge, Edinburgh and Imperial including formal specifications of C/C++ concurrency, OCaml light and the IBM POWER processor.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
