Home

Awesome

<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->

Huffman

Docker CI Contributing Code of Conduct Zulip coqdoc

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

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