CohenCyril/huffman

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.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

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

Documentation

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.

Running extracted code

To run the extracted algorithm, build the project and then 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;;