POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 14:45 - 15:10 at Auditorium - Gradual Typing and Contracts Chair(s): Ronald Garcia

Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing agenda and develop the notion of gradual refinement types, allowing smooth evolution and interoperability between simple types and logically-refined types. In doing so, we address two challenges unexplored in the gradual typing literature: dealing with imprecise logical information, and with dependent function types. The first challenge leads to a crucial notion of locality for refinement formulas, and the second yields novel operators related to type- and term-level substitution, identifying new opportunity for runtime errors in gradual dependently-typed languages. The gradual language we present is type safe, type sound, and satisfies the refined criteria for gradually-typed languages of Siek et al. We also explain how to extend our approach to richer refinement logics, anticipating key challenges to consider.

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Gradual Typing and ContractsPOPL at Auditorium
Chair(s): Ronald Garcia University of British Columbia
14:20
25m
Talk
Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
POPL
Michael Vitousek , Cameron Swords Indiana University, Jeremy G. Siek Indiana University Bloomington
14:45
25m
Talk
Gradual Refinement Types
POPL
Nicolás Lehmann , Éric Tanter University of Chile, Chile
Link to publication DOI Pre-print
15:10
25m
Talk
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
POPL
Matteo Cimini Indiana University, USA, Jeremy G. Siek Indiana University Bloomington
15:35
25m
Talk
Sums of Uncertainty: Refinements go gradual
POPL
Khurram A. Jafery University of British Columbia, Jana Dunfield University of British Columbia