符号理論・情報理論の形式化ライブラリinfotheoの情報をまとめています。
開発ヒストリ―
２００９年 Affeldt Reynald （産総研）が開発開始。
２０１０年 萩原学（当時：産総研、現：千葉大学）が参加。
シャノン理論の形式化のため、紙上で準形式証明の作成。
２０１２年 Jonas Sénizerguesが参加。
２０１３年 国際会議 ITPにて、シャノン理論の形式化の成功を発表。
プロジェクト「モダン符号の形式化」発足。
笠井健太（東工大）、葛岡成晃（和歌山大）、
溝口佳宏（九大IMI）、Jacques Garrigue（名大）、
才川隆文（名大）が参加。
２０１４年 小尾良介（当時：千葉大）が参加。
可変長情報源符号化定理の形式化担当。
２０１５年 中野恭輔（千葉大）が参加。
二元消失通信路の形式化担当。
２０１６年 通信路同型、BSECの形式化などをitEXT4CapOfChansに追加。
ダウンロード
◇公開中のライブラリinfotheo：
Coq8.5 with mathcom 1.6版はこちら。
◇infoTheoの追加パッケージ itEXT4CapOfChans：
Coq 8.5 with mathcomp 1.6版はこちら。
Coq 8.5 beta2 with SSReflect 1.5版はこちら。
BEC（二元消失通信路）の通信路容量、BSEC（二元対称消失通信路）の通信路容量、通信路同型の形式化などをまとめています。
おまけ
Coq/SSReflectを開発した INRIA のウェブページ「SSreflect in the world」に
infoTheoに関する論文がリンクされています。
