ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
Tue 3 Sep 2024 14:42 - 15:00 at Green 1-2-3 - Type Theory Chair(s): Brent Yorgey

Gradual typing integrates static and dynamic typing by introducing a dynamic type and a consistency relation. A problem of gradual type systems is that dynamic types can easily hide erroneous data flows since consistency relations are not transitive. Therefore, a more rigorous static check is required to reveal these hidden data flows statically. However, in order to preserve the expressiveness of gradually typed languages, static checks for gradually typed languages cannot simply reject programs with potentially erroneous data flows. By contrast, a more reasonable request is to show how these data flows can affect the execution of the program. In this paper, we propose and formalize Static Blame, a framework that can reveal hidden data flows for gradually typed programs and establish the correspondence between static-time data flows and runtime behavior. With this correspondence, we build a classification of potential errors detected from hidden data flows and formally characterize the possible impact of potential errors in each category on program execution, without simply rejecting the whole program. We implemented Static Blame on Grift, an academic gradually typed language, and evaluated the effectiveness of Static Blame by mutation analysis to verify our theoretical results. Our findings revealed that Static Blame exhibits a notable level of precision and recall in detecting type-related bugs. Furthermore, we conducted a manual classification to elucidate the reasons behind instances of failure. We also evaluated the performance of Static Blame, showing a quadratic growth in run time as program size increases.

Tue 3 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Type TheoryICFP Papers and Events / JFP First Papers at Green 1-2-3
Chair(s): Brent Yorgey Hendrix College
13:30
18m
Talk
Normalization by evaluation for modal dependent type theoryJFP First Paper
JFP First Papers
Jason Z.S. Hu McGill University, Junyoung Jang McGill University, Brigitte Pientka McGill University
DOI
13:48
18m
Talk
Closure-Free Functional Programming in a Two-Level Type Theory
ICFP Papers and Events
András Kovács University of Gothenburg
DOI Pre-print
14:06
18m
Talk
Gradual Indexed Inductive Types
ICFP Papers and Events
Mara Malewski Correa University of Chile, Kenji Maillard Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile
DOI
14:24
18m
Talk
Dependent Ghosts Have a Reflection for Free
ICFP Papers and Events
DOI
14:42
18m
Talk
Static Blame for gradual typingJFP First Paper
JFP First Papers
Chenghao Su Nanjing University, Lin Chen Nanjing University, Yanhui Li Nanjing University, Yuming Zhou Nanjing University
DOI