Tue 25 Jun 2019 16:00 - 16:20 at 228AB - Type Systems III Chair(s): Satish Chandra

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 Jun

Displayed time zone: Tijuana, Baja California change

16:00 - 16:40
Type Systems IIIPLDI Research Papers at 228AB
Chair(s): Satish Chandra Facebook
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
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