This program is tentative and subject to change.
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 JunDisplayed time zone: Seoul change
10:30 - 11:50 | |||
10:30 20mTalk | 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 20mTalk | 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 20mTalk | Practical Type Inference with Levels PLDI Research Papers DOI | ||
11:30 20mTalk | 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 |