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 Research Center), and was started by Reynald Affeldt, Manabu Hagiwara and Jonas Sénizergues.

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

See github for the latest version of the Coq source code!


Related documents: