Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm

    loading  Checking for direct PDF access through Ovid


Huffman's algorithm is a procedure for constructing a binary tree with minimum weighted path length. Our Isabelle/HOL 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.

Related Topics

    loading  Loading Related Articles