A library for formalization of linear error-correcting codes

DOI10.1007/s10817-019-09538-8zbMath1468.68314OpenAlexW3000218028WikidataQ126406119 ScholiaQ126406119MaRDI QIDQ2209551

Reynald Affeldt, Takafumi Saikawa, Jacques Garrigue

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09538-8

zbMATH Keywords

error-correcting codesCoqmathematical components

Mathematics Subject Classification ID

Linear codes (general theory) (94B05) Cyclic codes (94B15) Decoding (94B35) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formalization of Shannon's theorems
• Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
• Polynomial Codes Over Certain Finite Fields
• On a class of error correcting binary group codes
• Modern Coding Theory
• A method for solving key equation for decoding goppa codes
• Which codes have cycle-free Tanner graphs?
• The Theory of Information and Coding
• Factor graphs and the sum-product algorithm
• The capacity of low-density parity-check codes under message-passing decoding
• Error Detecting and Error Correcting Codes
• Finite-length analysis of low-density parity-check codes on the binary erasure channel
• A Machine-Checked Proof of the Odd Order Theorem