Differences

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

Link to this comparison view

Next revision		Previous revision
research:gsf [2021/02/09 14:38] – created mtororesearch:gsf [2021/02/09 15:52] (current) – elabrada
Line 1: Line 1:
 ====== GSF: Gradual System F ====== ====== 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|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.