Fully abstract from static to gradual

Koen Jacobs, Amin Timany, Dominique Devriese

Onderzoeksoutput: Article

2 Citaten (Scopus)
34 Downloads (Pure)


What is a good gradual language? Siek et al. have previously proposed the refined criteria, a set of formal ideas that characterize a range of guarantees typically expected from a gradual language. While these go a long way, they are mostly focused on syntactic and type safety properties and fail to characterize how richer semantic properties and reasoning principles that hold in the static language, like non-interference or parametricity for instance, should be upheld in the gradualization. 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. Rather than preserving an arbitrarily chosen interpretation of source language types, this criterion requires that all source language equivalences are preserved. We demonstrate that the criterion weeds out erroneous gradualizations that nevertheless satisfy the refined criteria. At the same time, we demonstrate that the criterion is realistic by reporting on a mechanized proof that the property holds for a standard example: GTLCμ, the natural gradualization of STLCμ, the simply typed lambda-calculus with equirecursive types. We argue thus that the criterion is useful for understanding, evaluating, and guiding the design of gradual languages, particularly those which are intended to preserve source language guarantees in a rich way.

Originele taal-2English
Pagina's (van-tot)1-30
Aantal pagina's30
TijdschriftProceedings of the ACM on Programming Languages
Nummer van het tijdschriftPOPL
StatusPublished - 4 jan 2021
EvenementPrinciples of Programming Languages -
Duur: 17 jan 202122 jan 2021


Duik in de onderzoeksthema's van 'Fully abstract from static to gradual'. Samen vormen ze een unieke vingerafdruk.

Citeer dit