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

Many language designers have adopted gradual typing. However, there remains open questions for them regarding how to gradualize their languages. Recently, a methodology and algorithm was proposed for generating the static semantics of a gradually typed language from a fully-static version of the language. In this paper, we address the more difficult challenge of how to automatically generate the dynamic semantics of gradually typed languages. Gradually-typed languages typically make use of an intermediate language with explicit casts, so we first offer a methodology for generating the syntax and type system of the intermediate language with casts.
Next, we present an algorithm that takes as input the dynamic semantics of the fully-static language and outputs the dynamic semantics for casts. We show that our approach is general enough to gradualize several languages, including features such as polymorphism, recursive types and exceptions. We prove that our algorithm produces cast languages that always satisfy the key correctness criteria of gradual typing. We implement these algorithms in a tool that can generate the complete specification of gradually typed languages in lambda-prolog, including their executable interpreters.

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Gradual Typing and ContractsPOPL at Auditorium
Chair(s): Ronald GarciaUniversity 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 SwordsIndiana University, Jeremy G. SiekIndiana University Bloomington
14:45
25m
Talk
Gradual Refinement Types
POPL
Nicolás Lehmann, Éric TanterUniversity of Chile, Chile
Link to publication DOI Pre-print
15:10
25m
Talk
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
POPL
Matteo CiminiIndiana University, USA, Jeremy G. SiekIndiana University Bloomington
15:35
25m
Talk
Sums of Uncertainty: Refinements go gradual
POPL
Khurram A. JaferyUniversity of British Columbia, Jana DunfieldUniversity of British Columbia