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

jorsn/infotheo

 
 

Repository files navigation

A Coq formalization of information theory and linear error correcting codes

Docker 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 (committers).

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 documented in changelog.txt.

Installation with Windows 10

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

Once MathComp is installed (with opam), do opam install coq-infotheo or git clone [email protected]: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.

About

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

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Coq 99.8%
  • Other 0.2%