Characterising renaming within OCaml's module system: theory and implementation

Reuben Rowe, Hugo Férée, Simon Thompson, Scott Owens

Research output: Chapter in Book/Report/Conference proceedingConference contribution

144 Downloads (Pure)

Abstract

We present an abstract, set-theoretic denotational semantics for a significant subset of OCaml and its module system, allowing to reason about the correctness of renaming value bindings. Our semantics captures information about the binding structure of programs, as well as about which declarations are related by the use of different language constructs (e.g. functors, module types and module constraints). Correct renamings are precisely those that preserve this structure. We show that our abstract semantics is sound with respect to a (domain-theoretic) denotational model of the operational behaviour of programs, and that it allows us to prove various high-level, intuitive properties of renamings. This formal framework has been implemented in a prototype refactoring tool for OCaml that performs renaming.
Original languageEnglish
Title of host publicationPLDI 2019
Subtitle of host publicationProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
PublisherAssociation for Computing Machinery (ACM)
Pages950-965
Number of pages16
ISBN (Print)978-1-4503-6712-7
DOIs
Publication statusPublished - 8 Jun 2019

Cite this