| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
The Textbook Proof of Huffman's Algorithm
| Title: | The Textbook Proof of Huffman's Algorithm |
| Author: | Jasmin Christian Blanchette (j /dot/ c /dot/ blanchette /at/ vu /dot/ nl) |
| 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{https://isa-afp.org/entries/Huffman.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | CakeML_Codegen |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |