Skip to content

A Coq formalization of information theory and linear error-correcting codes

License

Notifications You must be signed in to change notification settings

affeldt-aist/infotheo

Repository files navigation

A Coq formalization of information theory and linear error correcting codes

Docker CI Nix CI

Infotheo is a Coq library for reasoning about discrete probabilities, information theory, and linear error-correcting codes.

Meta

Building and installation instructions

The easiest way to install the latest released version of A Coq formalization of information theory and linear error correcting codes is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-infotheo

To instead build and install manually, do (using GNU make):

git clone https://github.com/affeldt-aist/infotheo.git
cd infotheo
make   # or make -j <number-of-cores-on-your-machine> 
make -C extraction tests
make install

Acknowledgments

Many thanks to several contributors.

The principle of inclusion-exclusion is a contribution by Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory) (main theorem: Pr_bigcup_incl_excl; commit 956096859ed89325b2bb74033690ac882bbcd64e)

The variable-length source coding theorems are a contribution by Ryosuke Obi (Chiba U. (M2)) (commit a67da5e24eaaabb345d225a5bd0f5e86d35413a8) (with Manabu Hagiwara and Mitsuharu Yamamoto)

Commit 64814f529c1819684c4b8060d0779c24c6339041 was originally by Karl Palmskog

The formalization of modern coding theory is a collaboration with K. Kasai, S. Kuzuoka, R. Obi

Y. Takahashi collaborated to the formalization of linear error-correcting codes

This work was partially supported by a JSPS Grant-in-Aid for Scientific Research (Project Number: 25289118), a JSPS Grand-in-Aid for Scientific Research (Project Number: 18H03204)

Documentation

Each file is documented in its header.

Changes are (lightly) documented in changelog.txt.

Installation with Windows 10 & 11

Installation of infotheo on Windows is less simple. See this page for instructions to install MathComp on Windows 10 & 11 (or this page for instructions in Japanese).

Once MathComp is installed (with opam), do opam install coq-infotheo or git clone git@github.com:affeldt-aist/infotheo.git; opam install .

Original License

Before version 0.2, infotheo was distributed under the terms of the GPL-3.0-or-later license.