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
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00: POPL - Gradual Typing and Contracts at Auditorium
Chair(s): Ronald GarciaUniversity of British Columbia
POPL-2017-papers14:20 - 14:45
Michael Vitousek, Cameron SwordsIndiana University, Jeremy G. SiekIndiana University Bloomington
POPL-2017-papers14:45 - 15:10
Nicolás Lehmann, Éric TanterUniversity of Chile, Chile
Link to publication DOI Pre-print
POPL-2017-papers15:10 - 15:35
Matteo CiminiIndiana University, USA, Jeremy G. SiekIndiana University Bloomington
POPL-2017-papers15:35 - 16:00
Khurram A. JaferyUniversity of British Columbia, Joshua DunfieldUniversity of British Columbia