Fully abstract from static to gradual

Koen Jacobs, Amin Timany, Dominique Devriese

Research output: Contribution to journalArticle

4 Downloads (Pure)

Abstract

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.

Original languageEnglish
Article number7
Pages (from-to)1-30
Number of pages30
JournalProceedings of the ACM on Programming Languages
Volume5
Issue numberPOPL
DOIs
Publication statusPublished - 4 Jan 2021
EventPrinciples of Programming Languages -
Duration: 17 Jan 202122 Jan 2021

Fingerprint Dive into the research topics of 'Fully abstract from static to gradual'. Together they form a unique fingerprint.

Cite this