Write a Blog >>
Sat 25 Jan 2020 09:30 - 10:00 at Orleans - Gradual Criteria Chair(s): Amal Ahmed

What is a good gradual language? Siek et al. have previously proposed the refined criteria, which specify certain guarantees about semantic correspondence and preservation of well-typedness and type-safety in the presence of untyped code. However, because of their exclusive focus on syntactic properties, they are not the whole story. Rich semantic properties like parametricity or non-interference, which hold in the static language, should also continue to hold upon gradualisation.

In this paper, we investigate and argue for a new criterion previously hinted at by Devriese et al.: the embedding from the static to the gradual language should be fully abstract. We illustrate in a simple setting that the criterion is useful; it can weed out an erroneous gradualisation that satisfies the refined criteria. We illustrate that it is realistic, by giving a proof sketch for the natural gradualisation of $\operatorname{STLC}_\mu$.

Conference Day
Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Gradual CriteriaWGT at Orleans
Chair(s): Amal AhmedNortheastern University, USA
09:00
30m
Talk
Gradual Typing as if Types Mattered
WGT
Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile
Pre-print
09:30
30m
Talk
Fully Abstract from Static to Gradual
WGT
Koen JacobsKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Dominique DevrieseVrije Universiteit Brussel
Pre-print