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.9.0.tar.gz
sha256=20b63eae0d17a23646446fcca22de945d6a19a03246bec8b5b4c8da6d6f3184b

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-05-15

Published: 15 May 2019

Dependencies (2)

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

Dev Dependencies

None

Used by

None

Conflicts

None