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