Formalization of Shannon's Theorem

The purpose of this webpage is to document a formalization of Shannon's theorems using the Mathematical Components library of the Coq proof-assistant.

We are investigating more generally formalization of information theory and of error-correcting codes (see these experiments for error-correcting codes).

This research first took place at the National Institute of Advanced Industrial Science and Technology, in the Research Institute for Secure Systems (now Information Technology Research Institute), and was started by Reynald Affeldt, Manabu Hagiwara and Jonas Sénizergues.

The formalization of the channel coding theorems follows: 萩原学, 符号理論デジタルコミュニケーションにおける数学, 日本評論社, 2012.

Coq source code:

Statements of Shannon Theorems in Coq:
Coq documentation (as of [2016-07-31 Sun]):
- index
- table of contents
Archives:
- [2017-10-27 Fri]: infotheo.tar.gz or infotheo.zip
  - Requirements: Coq 8.7, MathComp v1.6.2 (installed from source files or opam packages coq-mathcomp-{ssreflect,algebra,character,fingroup,field,solvable})
  - Installation: After gunzip/untar or unzip, do cd infotheo and coq_makefile -f MakeInfotheo_v1 -o Makefile and make.
    - You May need to add -I /xyz/math-comp/mathcomp and -R /xyz/math-comp/mathcomp mathcomp if MathComp is not at a standard location.
- [2016-02-02 Tue] archives (zip, tar.gz) for Coq 8.5 and MathComp 1.6, coq_makefile -f infotheo_make -o Makefile to generate the makefile
- [2015-11-19 Thu] archive for Coq 8.5beta2 and SSReflect/MatchComp v1.5beta2
Latest version: github