The other day, I was assembling lecture material for a course on Agda. Pursuing an application-driven approach, I was looking for correctness proofs of popular algorithms. One of my all-time favourites is Huffman data compression (Huffman, 1952). Even though it is probably safe to assume that you are familiar with this algorithmic gem, a brief reminder of the essential idea may not be amiss.

@article{paperbot2143,
  title = {Certified, total serialisers with an application to Huffman encoding},
  author = {RALF HINZE},
  journal = {Journal of Functional Programming},
  volume = {33},
  year = {2023},
  doi = {10.1017/s095679682200017x}
}