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