View publication

Title Gradual System F
Authors Elizabeth Labrada, Mat¿as Toro, Éric Tanter
Publication date October 2022
Abstract 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.
Pages 38:1-38:78
Volume 69
Journal name Journal of the ACM
Publisher ACM Press (New York, NY, USA)
Reference URL View reference page