package coq-huffman

  1. Overview
  2. No Docs
A 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.10.0.tar.gz
sha512=faeeaa47712a7b5df82ce1bc93db0e5c44b8398da71f3e7ce83d43b99b838c31734fd8226a7be39bf70ca75dbf5f0b6f9a516fea001282eadf3e22b7cfcd449d

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:2019-12-07

Published: 08 Dec 2019

Dependencies (2)

  1. coq >= "8.7" & < "8.12~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None