The Textbook Proof of Huffman's Algorithm

Jasmin Christian Blanchette 🌐

October 15, 2008

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Huffman's algorithm is a procedure for constructing a binary tree with minimum weighted path length. This report presents a formal proof of the correctness of Huffman's algorithm written using Isabelle/HOL. Our proof closely follows the sketches found in standard algorithms textbooks, uncovering a few snags in the process. Another distinguishing feature of our formalization is the use of custom induction rules to help Isabelle's automatic tactics, leading to very short proofs for most of the lemmas.

License

BSD License

Topics

Session Huffman