Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Last revisionBoth sides next revision
research:gsf [2021/02/09 14:39] – [GSF: Gradual System F] mtororesearch:gsf [2021/02/09 15:52] – elabrada
Line 1: Line 1:
-====== GSF: Gradual System F, Supplementary Material ======+====== GSF: Gradual System F ======
 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. 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 \sysF . 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.+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 {{bib>toroAl:popl2019|our POPL'19 paper}}.
  
 ====== Technical Report ====== ====== Technical Report ======
-Auxiliary definitions and proofs of the main results can be found in the [[http://www.google.com|companion technical report]].+Auxiliary definitions and proofs of the main results can be found in the 
 +{{research:tr.pdf| Gradual System F: companion technical report}}.
  
  
 ====== Prototype Implementation ====== ====== Prototype Implementation ======
-Additionally, an [[http://www.pleiad.cl/research/gsf/software|interactive prototype of GSF is available]], which exhibits both typing derivations and reduction traces, and comes with all the examples  mentioned in this paper, among others.+Additionally, an [[http://www.pleiad.cl/research/gsf/software|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.