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

proof-ninja/infotheo

This branch is 143 commits behind affeldt-aist/infotheo:master.

Folders and files

NameName
Last commit message
Last commit date
Jun 3, 2023
Feb 25, 2023
Jun 3, 2023
Jun 11, 2020
Sep 24, 2023
Sep 24, 2023
Sep 24, 2023
Dec 4, 2022
Feb 13, 2020
Feb 3, 2021
Dec 14, 2020
Nov 9, 2019
Jun 3, 2023
Dec 4, 2022
Sep 24, 2023
Jun 3, 2023
Dec 14, 2020
Dec 14, 2020
Dec 14, 2020
Jun 3, 2023

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 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.

About

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

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Coq 99.8%
  • Other 0.2%