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

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