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:

Coq source code:

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).