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.16.0.tar.gz
sha512=943db124e9f08afb1681754004ee5438f652f99cb6006bc7a4d390ce904090ed6344feaa31120a2f40728281a073ae0d720504607b86ac369001c610f83b3e7d

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:2023-07-09

Published: 01 Aug 2023

Dependencies (1)

  1. coq >= "8.12" & < "8.21"

Dev Dependencies

None

Used by

None

Conflicts

None