Authors: Josh Cohen and Palmer Paul
Abstract: We used LiquidHaskell to verify the structural invariants of binomial heaps and skew heaps and prove totality, termination, and functional correctness of all common heap operations on these structures. In this report, we describe the technical aspects of our project, challenges we faced, and our overall experience using LiquidHaskell. The code for our project is publicly available in the pzp1997/liquid-heaps GitHub repo.
See report.pdf for full paper.