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.
Tue 25 JunDisplayed time zone: Tijuana, Baja California change
16:00 - 16:40 | |||
16:00 20mTalk | Characterising Renaming within OCaml’s Module System: Theory and Implementation PLDI Research Papers Reuben N. S. Rowe University of Kent, Hugo Férée University of Kent, UK, Simon Thompson , Scott Owens University of Kent, UK Link to publication DOI Pre-print | ||
16:20 20mTalk | Type-Level Computations for Ruby Libraries PLDI Research Papers Milod Kazerounian University of Maryland, College Park, Sankha Narayan Guria University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Jeffrey S. Foster Tufts University, David Van Horn University of Maryland, USA Media Attached |