coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] New contribution: Huffman algorithm

From: Laurent Thery <Laurent.Thery AT sophia.inria.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] New contribution: Huffman algorithm
Date: Thu, 16 Oct 2003 13:08:37 +0200 (MET DST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Coq Users,

I'm happy to announce a formalisation in Coq of the Huffman
algorithm for data compression:

It is composed of :

- A proof of correctness of the algorithm as described in `A Method for the
Construction of Minimum-Redundancy Codes'.

- An extracted version of the algorithm that can be executed under ocaml

It is available at:

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Huffman/index.html

--
Laurent Thery

[Coq-Club] New contribution: Huffman algorithm, Laurent Thery