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.

• Author(s):
  • Laurent Théry (initial)
  • Karl Palmskog
• Coq-community maintainer(s):
  • Karl Palmskog (@palmskog)
• License: GNU Lesser General Public License v2.1 or later
• Compatible Coq versions: 8.12 or later
• Additional dependencies: none
• Coq namespace: Huffman
• Related publication(s):
  • Formalising Huffman's algorithm
  • A Method for the Construction of Minimum-Redundancy Codes doi:10.1109/JRPROC.1952.273898

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.git
cd huffman
make   # or make -j <number-of-cores-on-your-machine> 
make install

For more information about the project, see the technical report describing the formalization. See also the coqdoc presentation of the Coq source files from the latest release.

To extract code and obtain the program, run

make run_huffman.ml

Next, open an OCaml toplevel (e.g., 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;;