ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
Fri 6 Sep 2024 11:30 - 12:00 at Orange 3 - Haskell 1 Chair(s): Niki Vazou

Formal reasoning about the time complexity of algorithms and data structures is usually done in interactive theorem provers like Isabelle/HOL. This includes reasoning about \textit{amortized} time complexity which looks at the worst case performance over a \textit{series} of operations. However, most programs are not written within a theorem prover and thus use the data structures of the production language. To verify the correctness it is necessary to translate the data structures from the production language into the language of the prover. Such a translation step could introduce errors, for example due to a mismatch in features between the two languages.

We show how to prove amortized complexity of data structures directly in Haskell using LiquidHaskell. Besides skipping the translation step, our approach can also provide a didactic advantage. Learners do not have to learn an additional language for proofs and can focus on the new concepts only. For this paper, we do not assume prior knowledge of amortized complexity as we explain the concepts and apply them in our first case study, a simple stack with multipop. Moving to more complicated (and useful) data structures, we show that the same technique works for binomial heaps which can be used to implement a priority queue. We also prove amortized complexity bounds for Claessen’s version of the finger tree, a sequence-like data structure with constant-time cons/uncons on either end. Finally we discuss the current limitations of LiquidHaskell that made certain versions of the data structures not feasible.

Fri 6 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30
Haskell 1Haskell at Orange 3
Chair(s): Niki Vazou IMDEA Software Institute
11:00
30m
Talk
Haskelite: A Tracing Interpreter Based on a Pattern-Matching Calculus
Haskell
Pedro Vasconcelos University of Porto, Rodrigo Marques Universidade do Porto
11:30
30m
Talk
Liquid Amortization - Proving amortized complexity with LiquidHaskell (Functional Pearl)
Haskell
Jan van Brügge Heriot-Watt University
12:00
30m
Talk
Making a Curry Interpreter using Effects and Handlers
Haskell
Niels Bunkenburg University of Kiel, Germany, Nicolas Wu Imperial College London