This directory contains the Isabelle and LaTeX source files for the report "An
Isabelle/HOL Formalization of the Textbook Proof of Huffman’s Algorithm" by
Jasmin Christian Blanchette, originally released in October 2008.

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.