Email Gateway (Aug 18 2022 at 12:31): Email Gateway (Aug 18 2022 at 12:31):From: Tobias Nipkow <nipkow@in.tum.de>
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.
http://afp.sourceforge.net/entries/Huffman.shtml
Enjoy
Tobias
Last updated: May 03 2024 at 12:27 UTC