ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Thu 16 Oct 2025 11:05 - 11:35 at Peony SW - Types and monads Chair(s): Liam O'Connor

Persistent data structures are ubiquitous in functional programming languages and their designers frequently have to reason about amortized time complexity. But proving amortized bounds is difficult in a persistent setting, and pen-and-paper proofs give little assurance of correctness, while a full mechanization in a proof assistant can be too involved for the casual user. In this work, we define a strict domain specific language (DSL) for testing the amortized time complexity of persistent data structures using QuickCheck. Our DSL can give strong evidence of correctness, while imposing minimal overhead on the user. We have implemented all lazy data structures in Okasaki’s book in our DSL and have checked their amortized time complexity. We have also discovered and fixed a previously unreported gap in the analysis of persistent Finger Trees.

Thu 16 Oct

Displayed time zone: Perth change

10:30 - 12:15
Types and monadsHaskell at Peony SW
Chair(s): Liam O'Connor Australian National University
10:30
5m
Day opening
Welcome
Haskell
Ningning Xie University of Toronto, J. Garrett Morris University of Iowa
10:35
30m
Research paper
Freer Arrows and Why You Need Them in Haskell
Haskell
Grant VanDomelen Portland State University, USA, Gan Shen University of California at Santa Cruz, Lindsey Kuper University of California, Santa Cruz, Yao Li Portland State University
DOI Pre-print
11:05
30m
Research paper
Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad
Haskell
Anton Lorenzen University of Edinburgh
DOI
11:35
30m
Research paper
The Calculated Typer (Functional Pearl)
Haskell
Zac Garby University of Nottingham, Patrick Bahr IT University of Copenhagen, Graham Hutton University of Nottingham