Linear Error-correcting Codes in Coq
The purpose of this webpage is to document the formalization of linear error-correcting codes discussed in the following documents:
- Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
Formalization of Reed-Solomon codes and Progress Report on Formalization of LDPC codes.
International Symposium on Information Theory and Its Applications (ISITA 2016), October 30-November 2, 2016, Monterey, California, USA. IEICE. To appear.
- 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.
Coq source code:
- Coq documentation (as of 2016/08/18):
- Archive (as of 2017/01/06)
- Warning: this is a development version whose cleanup is in progress. It is suitable for browsing.
- Requirements: MathComp v1.6.1 and
- Installation: After
cd infotheo and do
coq_makefile -f MakeInfotheo -o Make and
make -f Make.
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).