Fully abstract from static to gradual

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

DOI

  • Koen Jacobs, KU Leuven
  • ,
  • Amin Timany
  • Dominique Devriese, Vrije Universiteit Brussel

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
JournalProceedings of the ACM on Programming Languages
Volume5
IssuePOPL
Number of pages30
DOIs
Publication statusPublished - Jan 2021

Bibliographical note

Funding Information:
This work was funded in part by Internal Funds KU Leuven grant C14/18/064. Amin Timany was a postdoctoral fellow of the Flemish research fund (FWO) during parts of this project. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0054. This work was partly supported by the Fund for Scientific Research - Flanders (FWO).

Publisher Copyright:
© 2021 Owner/Author.

Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.

    Research areas

  • fully abstract compilation, fully abstract embedding, gradual typing

See relations at Aarhus University Citationformats

ID: 208206433