Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory

DOI10.1007/978-3-319-22102-1_2zbMath1465.94146OpenAlexW2126522777MaRDI QIDQ2945620

Jacques Garrigue, Reynald Affeldt

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_2

Mathematics Subject Classification ID

Theory of error-correcting codes and error-detecting codes (94B99) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (3)

Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory ⋮ A library for formalization of linear error-correcting codes

Uses Software

• Coq
• Coq/SSReflect

Cites Work

• Certifying assembly with formal security proofs: the case of BBS
• Formalization of Shannon's theorems
• Error-correcting linear codes. Classification by isometry and applications. With CD-ROM
• A Refinement-Based Approach to Computational Algebra in Coq
• Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
• Modern Coding Theory
• Which codes have cycle-free Tanner graphs?
• Factor graphs and the sum-product algorithm
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory