The Textbook Proof of Huffman's Algorithm

Title:	The Textbook Proof of Huffman's Algorithm
Author:	Jasmin Christian Blanchette
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.
Status: [ok]	This is the development version of this entry generated for Isabelle-16-Sep-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

Older releases: