POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 17:30 - 17:50 at Kelvin Lecture - Gradual Typing and Verification Chair(s): Ronald Garcia

Gradual typing has emerged as a popular design point in programming languages, attracting significant interests from both academia and industry. Programmers in gradually typed languages are free to utilize static and dynamic typing as needed. To make such languages sound, runtime checks mediate the boundary of typed and untyped code. Unfortunately, such checks can incur significant runtime overhead on programs that heavily mix static and dynamic typing. To combat this overhead without necessitating changes to the underlying implementations of languages, we present discriminative typ ing. Discriminative typing works by optimistically inferring types for functions and implementing an optimized version of the function based on this type. To preserve safety it also implements an un-optimized version of the function based purely on the provided annotations. With two versions of each function in hand, discriminative typing translates programs so that the optimized functions are called as frequently as possible while also preserving program behaviors.

We have implemented discriminative typing in Reticulated Python and have evaluated its performance compared to guarded Reticulated Python. Our results show that discriminative typing improves the perfor- mance across 95% of tested programs, when compared to Reticulated, and achieves more than 4× speedup in more than 56% of these programs. We also compare its performance against a previous optimization approach and find that discriminative typing improved performance across 93% of tested programs, with 30% of these programs receiving speedups between 4 to 25 times. Finally, our evaluation shows that discriminative typing remarkably reduces the overhead of gradual typing on many mixed type configurations of programs.

In addition, we have implemented discriminative typing in Grift and evaluated its performance. Our evaluation demonstrations that DT significantly improves performance of Grift.

Fri 19 Jan

Displayed time zone: London change

16:50 - 18:10
Gradual Typing and VerificationPOPL at Kelvin Lecture
Chair(s): Ronald Garcia University of British Columbia
16:50
20m
Talk
Securing Verified IO Programs Against Unverified Code in F*
POPL
Cezar-Constantin Andrici MPI-SP, Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Cătălin Hriţcu MPI-SP, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology, Éric Tanter University of Chile, Théo Winterhalter INRIA Saclay
Pre-print
17:10
20m
Talk
Sound Gradual Verification with Symbolic Execution
POPL
Conrad Zimmerman Brown University, Jenna DiVincenzo (Wise) Purdue University, Jonathan Aldrich Carnegie Mellon University
17:30
20m
Talk
Type-based Gradual Typing Performance Optimization
POPL
John Peter Campora Quantinuum, Mohammad Wahiduzzaman Khan UL Lafayette, Sheng Chen UL Lafayette
17:50
20m
Talk
Total Type Error Localization and Recovery with HolesDistinguished Paper
POPL
Eric Zhao University of Michigan, Raef Maroof University of Michigan, Anand Dukkipati University of Michigan, Andrew Blinn University of Michigan, Zhiyi Pan University of Michigan, Cyrus Omar University of Michigan