thery/huffman

A correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]

Huffman

This projects contains a Coq proof of the correctness of the Huffman coding algorithm, as described in David A. Huffman's paper A Method for the Construction of Minimum-Redundancy Codes, Proc. IRE, pp. 1098-1101, September 1952.

Meta

• Author(s):
  • Laurent Théry (initial)
• Coq-community maintainer(s):
  • Karl Palmskog (@palmskog)
• License: GNU Lesser General Public License v2.1 or later
• Compatible Coq versions: 8.7 or later
• Additional Coq dependencies: none

Building and installation instructions

The easiest way to install the latest released version of Huffman is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-huffman

To instead build and install manually, do:

git clone https://github.com/coq-community/huffman
cd huffman
make   # or make -j <number-of-cores-on-your-machine>
make install

After installation, the included modules are available under the Huffman namespace.

Documentation

To run the algorithm, open an OCaml toplevel (ocaml) and do

#use "run_huffman.ml";;

To get the code that gives the frequency string:

let code = huffman "abbcccddddeeeee";;

To code a string:

let c = encode code "abcde";;

To decode a string:

decode code c;;

Some more information on the development is available: ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/Huffman/index.html

A technical report describes the formalization

See also the paper on the algorithm.