Write a Blog >>
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: Saskatchewan, Central America change

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