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

pldi-2019-papers
16:00 - 16:40: PLDI Research Papers - Type Systems III at 228AB
Chair(s): Satish ChandraFacebook
pldi-2019-papers16:00 - 16:20
Talk
Reuben N. S. RoweUniversity of Kent, Hugo FéréeUniversity of Kent, UK, Simon Thompson, Scott OwensUniversity of Kent, UK
Link to publication DOI Pre-print
pldi-2019-papers16:20 - 16:40
Talk
Milod KazerounianUniversity of Maryland, College Park, Sankha Narayan GuriaUniversity of Maryland, College Park, Niki VazouIMDEA Software Institute, Jeffrey S. FosterTufts University, David Van HornUniversity of Maryland, USA
Media Attached