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. |
| Downloaded | 7 times |
| Pages | 38:1-38:78 |
| Volume | 69 |
| Journal name | Journal of the ACM |
| Publisher | ACM Press (New York, NY, USA) |
|
|
| Reference URL |
|