Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs have been recently proposed, with varying syntax, behavior, and properties. Starting from a detailed review of the challenges and tensions that affect the design of gradual parametric languages, this work presents an extensive account of the semantics and metatheory of GSF, a gradual counterpart of System F. In doing so, we also report on the extent to which the Abstracting Gradual Typing methodology can help us derive such a language. Among gradual parametric languages that follow the syntax of System F, GSF achieves a unique combination of properties. We clearly establish the benefits and limitations of the language, and discuss several extensions of GSF towards a practical programming language.

This page provides access to the supplementary material accompanying our current submission, which extends our POPL'19 paper.

Auxiliary definitions and proofs of the main results can be found in the companion technical report.

Additionally, an interactive prototype of GSF is available, which exhibits both typing derivations and reduction traces, and comes with all the examples mentioned in the paper, among others.