Sat 25 Jan 2020 11:00 - 11:30 at Orleans - Programming features Chair(s): Giuseppe Castagna

This work studies gradual typing for row types and row polymorphism. Key ingredients in this work are the \emph{dynamic row type}, which represents a statically unknown part of a row, and \emph{consistency for row types}, which allows injecting static row types into the dynamic row type and, conversely, projecting the dynamic row type to any static row type. While consistency captures the behavior of the dynamic row type statically, it makes the semantics of a gradually typed language incoherent when combined with row equivalence which identifies row types up to field reordering. To solve this problem, we develop \emph{consistent equivalence}, which characterizes composition of consistency and row equivalence. Using consistent equivalence, we propose a polymorphic blame calculus $\text{F}^\rho_\text{C}$ for row types and row polymorphism. In $\text{F}^\rho_\text{C}$, casts perform not only run-time checking with the dynamic row type but also field reordering in row types. To simplify our technical development for row polymorphism, we adopt \emph{scoped} labels, which are employed by the language Koka and are also emerging in the context of effect systems. We give the formal definition of $\text{F}^\rho_\text{C}$ with these technical developments and prove its type soundness. We also sketch the gradually typed surface language $\text{F}^\rho_\text{G}$ and type-preserving translation from $\text{F}^\rho_\text{G}$ to $\text{F}^\rho_\text{C}$ and discuss conservativity of $\text{F}^\rho_\text{G}$ over typing of a statically typed language with row types and row polymorphism.

#### Sat 25 JanDisplayed time zone: Saskatchewan, Central America change

 10:30 - 12:30 Programming featuresWGT at Orleans Chair(s): Giuseppe Castagna CNRS - Université de Paris, France 10:3030mTalk Gradual Algebraic Data TypesWGTMichael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile Pre-print File Attached 11:0030mTalk Gradual Typing for Extensibility by RowsWGTTaro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan Pre-print 11:3030mTalk Foreign Function Typing: Semantic Type Soundness for FFIsWGTDaniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA Pre-print 12:0030mTalk Space-Efficient Monotonic ReferencesWGTDeyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA Pre-print