View the project on GitHub
Welcome to the Huffman project website! This project is part of coq-community.
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.
This is an open source project, licensed under the GNU Lesser General Public License v2.1 or later.
The current stable release of Huffman can be downloaded from GitHub.
The coqdoc presentations of releases can be browsed online:
Other related publications, if any, are listed below.