ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Mon 4 Sep 2023 12:07 - 12:30 at St Helens - TyDe: Type-Driven Types Chair(s): Reynald Affeldt

We present a novel row-polymorphic record calculus, supporting a unique combination of features: scoped labels, first-class labels and rows, and record concatenation. Our work is motivated by the similarity of record types and data table (or data frame) schemas, commonly used in data processing tasks. After presenting our record calculus, we demonstrate its applicability to data frame manipulation by showing that it can be used to successfully assign types to the functions listed in the Brown Benchmark for Tabular Types. Our typing discipline is remarkably lightweight, compared to calculi that require reasoning about type-level constraints when manipulating record types, making it a viable candidate for practical use.

Mon 4 Sep

Displayed time zone: Pacific Time (US & Canada) change

11:00 - 12:30
TyDe: Type-Driven TypesTyDe at St Helens
Chair(s): Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan
11:00
22m
Talk
A Calculus of Inductive Linear Constructions
TyDe
Qiancheng Fu Boston University, Hongwei Xi Boston University
DOI
11:22
22m
Talk
A Dependently Typed Language with Dynamic Equality
TyDe
Mark Lemay Autodesk, Qiancheng Fu Boston University, William Blair Boston University, Cheng Zhang Boston University, Hongwei Xi Boston University
DOI
11:45
22m
Talk
Combining Dependency, Grades, and Adjoint Logic
TyDe
Peter Hanukaev Augusta University, Harley D. Eades III Augusta University
DOI
12:07
22m
Talk
Infix-Extensible Record Types for Tabular DataRecorded
TyDe
Adam Paszke Google Research, Ningning Xie University of Toronto / Google DeepMind
DOI