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 also investigating more generally formalization of information theory and of error-correcting codes (see for example these experiments in progress).
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 ):
- Archive (as of 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
orunzip
, docd infotheo
and docoq_makefile -f MakeInfotheo_v1 -o Makefile
andmake
.- 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.
- You May need to add
- Older versions: 2016/02/02 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 archive for Coq 8.5beta2 and SSReflect/MatchComp v1.5beta2
): - Requirements: Coq 8.7, MathComp v1.6.2 (installed from source files or opam packages
Related documents:
- ITP 2015 paper
- JAR 2014 article
- IEICE 2013 presentation
- IMI 2013 lecture
- Suusemi 2013
- ITP 2012 paper
This research was partially supported by a Grant-in-Aid for Scientific Research Number 25289118, Kakenhi B, Formalization of Modern Coding Theory (
- ).