Characterising renaming within OCaml's module system : theory and implementation. / Rowe, Reuben; Férée, Hugo; Thompson, Simon; Owens, Scott.

PLDI 2019 Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery (ACM), 2019. p. 950-965.

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

Published

Documents

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 Proceedings 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
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 34708446