README.org
May 30, 2019 ยท View on GitHub
- infotheo
This is a Coq formalization of information theory and linear error-correcting codes.
** Requirements
- [[https://coq.inria.fr][Coq]] 8.9.0 or 8.9.1
- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.8.0
- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.2.0
which requires
- [[https://github.com/math-comp/bigenough/][bigenough]] first release
- [[https://github.com/math-comp/finmap][finmap]] 1.2.0
All versions available from opam.
See branch mathcomp-1.9.0 [2019-05-30 Thu] for a version compatible with mathcomp 1.9.0, analysis 0.2.2, finmap 1.2.1.
** Installation
coq_makefile -f _CoqProject -o Makefilemakemake install(if needed in another project)
** License
GNU GPLv3
** Authors
See [[infotheo_authors.txt]]
** References
There are a few papers available [[https://staff.aist.go.jp/reynald.affeldt/shannon/][here]] (information theory) and [[https://staff.aist.go.jp/reynald.affeldt/ecc/][here]] (error-correcting codes) that provide explanations and references.