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 Jan Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

 10:30 - 12:30: WGT - Programming features at Orleans Chair(s): Giuseppe CastagnaCNRS - Université de Paris, France 10:30 - 11:00Talk Gradual Algebraic Data TypesMichael GreenbergPomona College, Stefan MalewskiUniversity of Santiago de Chile, Éric TanterUniversity of Chile Pre-print File Attached 11:00 - 11:30Talk Gradual Typing for Extensibility by RowsTaro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan Pre-print 11:30 - 12:00Talk Foreign Function Typing: Semantic Type Soundness for FFIsDaniel PattersonNortheastern University, Amal AhmedNortheastern University, USA Pre-print 12:00 - 12:30Talk Space-Efficient Monotonic ReferencesDeyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA Pre-print