package coq-huffman
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Coq proof of the correctness of the Huffman coding algorithm
Install
Dune Dependency
Authors
Maintainers
Sources
v8.13.0.tar.gz
sha512=7a38feed6b2757badaf696729287bf5df7a8786e97e3133faf647335ab36ecd7c83caa8c359288d4b8dff89012bdc240a9eb548f3ffe3dc5757244d4ea0f9b78
Description
This projects contains a Coq proof of the correctness of the Huffman coding algorithm, as described in David A. Huffman's paper A Method for the Construction of Minimum-Redundancy Codes, Proc. IRE, pp. 1098-1101, September 1952.
Tags
category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Miscellaneous/Extracted Programs/Combinatorics keyword:data compression keyword:code keyword:huffman tree logpath:Huffman date:2021-07-30Published: 30 Jul 2021
On This Page