Characterising renaming within OCaml’s module system: theory and implementation
- Submitting institution
-
The University of Kent
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 16271
- Type
- E - Conference contribution
- DOI
-
10.1145/3314221.3314600
- Title of conference / published proceedings
- Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2019
- First page
- 950
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- June
- Year of publication
- 2019
- URL
-
https://kar.kent.ac.uk/73526/
- 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
-
3
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper is significant because it describes a novel formal renaming framework for OCaml, formalised in the Coq proof assistant. The work is implemented in the open source ROTOR refactoring tool. The tool and proofs, built with industrial input from Jane Street Capital, passed the PLDI artefact evaluation process. Since publication, ROTOR has been integrated with Dune, the OCaml build system, making it part of the standard development workflow.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
