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: 萩原学, 符号理論 デジタルコミュニケーションにおける数学, 日本評論社, 2012.

Coq source code:

• Statements of Shannon Theorems in Coq:
  • Source Coding direct
  • Source Coding converse
  • Channel Coding direct
  • Channel Coding converse
• Coq documentation (as of 2016/07/31):
  • index
  • table of contents
• 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 gunzip/untar, do 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

Related documents:

• 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.
• Reynald Affeldt. 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.
• Reynald Affeldt. 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. pdf. scripts.tar.gz.
• AFFELDT Reynald. 形式的な符号理論に向けて. 数学セミナー 618:74-79. 日本評論社, 2013年4月.
• 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).