Certified, total serialisers with an application to Huffman encoding

Reference. Certified, total serialisers with an application to Huffman encoding

Ralf Hinze · JFP · 2023 · PDF · DOI · pldb

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.

Cite

Cite as @hinze-2023-certified (helia, typst) · \cite{hinze-2023-certified} (LaTeX)

BibTeX

bibtex · 1 line

@article{hinze-2023-certified, title={Certified, total serialisers with an application to Huffman encoding}, volume={33}, ISSN={1469-7653}, url={http://dx.doi.org/10.1017/s095679682200017x}, DOI={10.1017/s095679682200017x}, journal={Journal of Functional Programming}, publisher={Cambridge University Press (CUP)}, author={HINZE, RALF}, year={2023} }

hayagriva YAML (typst)

yaml · 14 lines

hinze-2023-certified:
  type: article
  title: Certified, total serialisers with an application to Huffman encoding
  author: HINZE, RALF
  date: 2023
  url: http://dx.doi.org/10.1017/s095679682200017x
  serial-number:
    doi: 10.1017/s095679682200017x
    issn: 1469-7653
  parent:
    type: periodical
    title: Journal of Functional Programming
    publisher: Cambridge University Press (CUP)
    volume: 33

Download: hinze-2023-certified.bib · hinze-2023-certified.yml

Cites 6 works (1 here)

With notes (1)

agdarsec — total parser combinators allais_2018JFLA · 2018

Web

External (5)

Verified Functional Programming in Agda (2016)
Formalising Huffman's algorithm (2004)
Polytypic data conversion programs (2002)
A novel representation of lists and its application to the function “reverse” (1986)
A method for the construction of minimum-redundancy codes (1952)