Liquid types can express richer verification properties than simple type systems. However, despite their advantages, liquid types have yet to achieve widespread adoption. To understand why, we conducted a study analyzing developers' challenges with liquid types, focusing on LiquidHaskell.
Our findings reveal nine key barriers that span three categories, including developer experience, scalability challenges with complex and large codebases, and understanding the verification process. Together, these obstacles provide a comprehensive view of the usability challenges to the broader adoption of liquid types and offer insights that can inform the current and future design and implementation of liquid type systems.
Fri 20 JunDisplayed time zone: Seoul change
Fri 20 Jun
Displayed 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 LevelsDistinguished Paper 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 | ||