This directory contains the Isabelle and LaTeX source files for the report "An Isabelle/HOL Formalization of the Textbook Proof of Huffman’s Algorithm"by
Jasmin Christian Blanchette, originally released in October 2008.
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 tohelp Isabelle's automatic tactics, leading to very
short proofs for most of the lemmas.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
Suchen
