Skip to main content

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)

PDF Author's Accepted Manuscript
Language: English
Download (1MB)
[thumbnail of paper (1).pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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: (The current URI for this page, for reference purposes)
Rowe, Reuben:
Thompson, Simon:
Owens, Scott:
  • Depositors only (login required):


Downloads per month over past year