Fully Abstract from Static to Gradual
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 STLCμ.
The bibtex source for this publication:
@inproceedings{WGT20_full_abs,
author = {Koen Jacobs and Amin Timany and Dominique Devriese},
title = {{Fully Abstract from Static to Gradual}},
booktitle = {Workshop on Gradual Typing},
year = {2020},
month = {January},
url = {https://popl20.sigplan.org/home/wgt-2020}
}