[isabelle] New AFP article: Huffman's Algorithm

Thanks to Jasmin Blanchette we have a new article:

The Textbook Proof of Huffman's Algorithm

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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.