Formalization of Shannon's Theorems
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:
萩原学, 符号理論 デジタルコミュニケーションにおける数学,
Coq source code:
- Statements of Shannon Theorems in Coq:
- Coq documentation (as of 2016/07/31):
- Archive (as of 2017/01/06)
- Requirements: Coq 8.6, MatchComp v1.6.1 (coq-mathcomp-ssreflect, coq-mathcomp-algebra, coq-mathcomp-character, coq-mathcomp-field, coq-mathcomp-solvable)
- Installation: After
cd infotheo and do
coq_makefile -f MakeInfotheo_v1 -o Make and
make -f 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.
- Older versions: 2016/02/02 archive for Coq 8.5 and MathComp 1.6,
coq_makefile -f infotheo_make -o Make to generate the makefile; 2015/11/19 archive for Coq 8.5beta2 and SSReflect/MatchComp v1.5beta2
Reynald Affeldt and Jacques Garrigue.
Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory. In 6th Conference on Interactive Theorem Proving (ITP 2015), August 24-27, 2015, Nanjing, China, volume 9236 of Lecture Notes in Computer Science, pages 17-33. Springer, August 2015. pdf.
Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues.
Formalization of Shannon’s Theorems.
Journal of Automated Reasoning, 53(1):63-103, 2014. Springer. Springer Link. preprint.
Formalization of Shannon's Theorems Using the Coq Proof-Assistant.
IEICE Society Conference 2013,
Fukuoka Institute of Technology.
Tutorial. pdf (contains some Japanese characters). Technical Committee on Information Theory, 18/09/2013.
About the Formal Verification of Shannon's Theorems.
In From Modern Coding Theory To Postmodern Coding Theory,
March 4-7, 2013, Fukuoka, Japan,
volume 44 of Math-for-Industry Lecture Notes, pages 86-94.
Invited lecture. Kyushu University, 01/30/2013.
Reynald Affeldt and Manabu Hagiwara.
Formalization of Shannon's Theorems in SSReflect-Coq. In 3rd Conference on Interactive Theorem Proving (ITP 2012), August 13-15, 2012, Princeton, New Jersey, USA, volume 7406 of Lecture Notes in Computer Science, pages 233-249. Springer, August 2012. preprint. slides.
This research was partially supported by a Grant-in-Aid for Scientific Research Number 25289118, Kakenhi B, Formalization of Modern Coding Theory (2013/04/01-2016/03/31).