package coq-huffman

  1. Overview
  2. No Docs
Coq proof of the correctness of the Huffman coding algorithm

Install

Dune Dependency

github.com Edit opam file Versions (12)

Authors

  1. L
    Laurent Théry

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.12.0.tar.gz
sha512=644b12056d2d9e68b4a2b0af7106885467aec28d44da5933a1d3b506925a5876611242570c0a70e019b4ed59ba64c1d6f52d7218b43dd82ae3a6f631a6a86d66

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:2020-07-26

Published: 04 Aug 2020

Dependencies (1)

  1. coq >= "8.7" & < "8.13~"

Dev Dependencies

None

Used by

None

Conflicts

None