Formalization of Shannon's theorems in SSReflect-Coq

DOI10.1007/978-3-642-32347-8_16zbMATH Open1314.68270OpenAlexW2099474694MaRDI QIDQ2914745FDOQ2914745

Authors: Reynald Affeldt, Manabu Hagiwara 

Publication date: 20 September 2012

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

Full work available at URL: https://doi.org/10.1007/978-3-642-32347-8_16

Recommendations

• Formalization of Shannon's theorems
• Formalization of entropy measures in HOL
• scientific article; zbMATH DE number 3894969
• Formal analysis of information flow in HOL
• A combinatorial lemma and Shannon's theorem for binary symmetric channels

Mathematics Subject Classification ID

Measures of information, entropy (94A17) Coding theorems (Shannon theory) (94A24)

Cited In (2)

• Formalization of Shannon's theorems
• Formalization of entropy measures in HOL

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: Formalization of Shannon's theorems in SSReflect-Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914745)