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:

Related documents:

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 Mon]-[2016-03-31 Thu]).