| title | lang | header-includes | |
|---|---|---|---|
A Coq formalization of information theory and linear error correcting codes |
en |
|
Welcome to the A Coq formalization of information theory and linear error correcting codes project website!
Infotheo is a Coq library for reasoning about discrete probabilities, information theory, and linear error-correcting codes.
This is an open source project, licensed under the LGPL-2.1-or-later.
The current stable release of A Coq formalization of information theory and linear error correcting codes can be downloaded from GitHub.
Related publications, if any, are listed below.
- Formal Adventures in Convex and Conical Spaces doi:10.1007/978-3-030-53518-6_2
- A Library for Formalization of Linear Error-Correcting Codes doi:10.1007/s10817-019-09538-8
- Reasoning with Conditional Probabilities and Joint Distributions in Coq doi:10.11309/jssst.37.3_79
- Examples of formal proofs about data compression doi:10.23919/ISITA.2018.8664276
- Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes
- Formalization of error-correcting codes---from Hamming to modern coding theory doi:10.1007/978-3-319-22102-1_2
- Formalization of Shannon’s Theorems doi:10.1007/s10817-013-9298-1
- Report issues on GitHub
- Reynald Affeldt, AIST
- Manabu Hagiwara, Chiba U. (previously AIST)
- Jonas Senizergues, ENS Cachan (internship at AIST)
- Jacques Garrigue, Nagoya U.
- Kazuhiko Sakaguchi, Tsukuba U.
- Taku Asai, Nagoya U. (M2)
- Takafumi Saikawa, Nagoya U.
- Naruomi Obata, Titech (M2)