Skip to main content
Kent Academic Repository

Characterising Renaming within OCaml’s Module System: Theory and Implementation

Rowe, Reuben, Férée, Hugo, Thompson, Simon, Owens, Scott (2019) Characterising Renaming within OCaml’s Module System: Theory and Implementation. In: PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '19: ACM SIGPLAN Conference on Programming Language Design and Implementation Proceedings. . pp. 950-965. ACM, ACM New York, NY, USA ©2019 ISBN 978-1-4503-6712-7. (doi:10.1145/3314221.3314600) (KAR id:73526)

Abstract

We present an abstract, set-theoretic denotational semantics

for a significant subset of OCaml and its module system

in order to reason about the correctness of renaming value

bindings. Our abstract semantics captures information about

the binding structure of programs. Crucially for renaming, it

also captures information about the relatedness of different

declarations that is induced by the use of various different

language constructs (e.g. functors, module types and module constraints). Correct renamings are precisely those that

preserve this structure. We demonstrate that our semantics

allows us to prove various high-level, intuitive properties

of renamings. We also show that it is sound with respect to

a (domain-theoretic) denotational model of the operational

behaviour of programs. This formal framework has been

implemented in a prototype refactoring tool for OCaml that

performs renaming

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1145/3314221.3314600
Uncontrolled keywords: Adequacy, denotational semantics, dependencies, modules, module types, OCaml, refactoring, renaming, static semantics
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Reuben Rowe
Date Deposited: 17 Apr 2019 15:34 UTC
Last Modified: 09 Dec 2022 07:33 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/73526 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.