PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Fri 20 Jun 2025 11:10 - 11:30 at Grand Ball Room 2 - Type Systems

Modern functional languages rely on sophisticated type inference algorithms. However, there often exists a gap between the theoretical presentation of these algorithms and their practical implementations. Specifically, implementations employ techniques not explicitly included in formal specifications, causing undesirable consequences. First, this leads to confusion and unforeseen challenges for developers adhering to the formal specification. Moreover, theoretical guarantees established for a formal presentation may not directly translate to the implementation. This paper focuses on formalizing one such technique, known as levels, which is widely used in practice but whose theoretical treatment remains largely understudied. We present the first comprehensive formalization of levels and demonstrate their applicability to type inference implementations.

This program is tentative and subject to change.

Fri 20 Jun

Displayed time zone: Seoul change

10:30 - 11:50
10:30
20m
Talk
Usability Barriers for Liquid Types
PLDI Research Papers
Catarina Gamboa Carnegie Mellon University and University of Lisbon, Abigail Elena Reese Carnegie Mellon University, Alcides Fonseca LASIGE; University of Lisbon, Jonathan Aldrich Carnegie Mellon University
DOI Pre-print
10:50
20m
Talk
Dynamic Region Ownership for Concurrency Safety
PLDI Research Papers
Fridtjof Stoldt Uppsala University, Brandt Bucher Microsoft, Sylvan Clebsch Microsoft Azure Research, Matthew A. Johnson Microsoft Azure Research, Matthew J. Parkinson Microsoft Azure Research, Guido van Rossum Microsoft, Eric Snow Microsoft, Tobias Wrigstad Uppsala University
DOI
11:10
20m
Talk
Practical Type Inference with Levels
PLDI Research Papers
Andong Fan University of Toronto, Han Xu Princeton University, Ningning Xie University of Toronto
DOI
11:30
20m
Talk
Thrust: A Prophecy-Based Refinement Type System for Rust
PLDI Research Papers
Hiromi Ogawa University of Tsukuba, Taro Sekiyama National Institute of Informatics, Hiroshi Unno Tohoku University
DOI