The Textbook Proof of Huffman's Algorithm

 

Title: The Textbook Proof of Huffman's Algorithm
Author: Jasmin Christian Blanchette (jasmin /dot/ blanchette /at/ gmail /dot/ com)
Submission date: 2008-10-15
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.
BibTeX:
@article{Huffman-AFP,
  author  = {Jasmin Christian Blanchette},
  title   = {The Textbook Proof of Huffman's Algorithm},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2008,
  note    = {\url{http://isa-afp.org/entries/Huffman.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License