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

Displayed time zone: Saskatchewan, Central America change

10:30 - 12:30
Programming featuresWGT at Orleans
Chair(s): Giuseppe Castagna CNRS - Université de Paris, France
10:30
30m
Talk
Gradual Algebraic Data Types
WGT
Michael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile
Pre-print File Attached
11:00
30m
Talk
Gradual Typing for Extensibility by Rows
WGT
Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Pre-print
11:30
30m
Talk
Foreign Function Typing: Semantic Type Soundness for FFIs
WGT
Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA
Pre-print
12:00
30m
Talk
Space-Efficient Monotonic References
WGT
Deyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA
Pre-print