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

Dependent type systems are powerful tools for preventing bugs in programs.
Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs.
However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories.
We address this issue by designing a dependently typed language where equality checking is delayed until runtime.
What were once static errors can now be presented to programmers as warnings.
When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution.
We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language.
Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage.
Finally, we have implemented a prototype of the language.

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
DOI