Formalization of Information Theory

The purpose of this webpage is to document a formalization of information theory (including Shannon's theorems) and of linear error-correcting codes using the Mathematical Components library of the Coq proof-assistant.

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

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

Coq source code:

• Latest version: github
• 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

Related documents:

• ISITA 2018 paper
• ISITA 2016 paper
• ITP 2015 paper
• JAR 2014 article
• IEICE 2013 presentation
• IMI 2013 lecture
• Suusemi 2013
• ITP 2012 paper

Acknowledgements:

• Grant-in-Aid for Scientific Research Number 18H03204, Kakenhi B ([2018-04-01 Sun]-[2021-03-31 Wed])
• Grant-in-Aid for Scientific Research Number 25289118, Kakenhi B, Formalization of Modern Coding Theory ([2013-04-01 Mon]-[2016-03-31 Thu])