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.15.0.tar.gz
sha512=06b6147a713e3f15428623ab09c9f226e626837a9e1876892a24ebdc1843c84ade0ccd8aafe53892b899dc235ff42d0e3cc11e4bd324f3ebb57e205e4fdf6a9d

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:2022-06-19

Published: 19 Jun 2022

Dependencies (1)

  1. coq >= "8.12" & < "8.17~"

Dev Dependencies

None

Used by

None

Conflicts

None