Formalization of Shannon's theorems
From MaRDI portal
Publication:2352494
DOI10.1007/s10817-013-9298-1zbMath1315.68216OpenAlexW2068110684MaRDI QIDQ2352494
Reynald Affeldt, Jonas Sénizergues, Manabu Hagiwara
Publication date: 2 July 2015
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-013-9298-1
Related Items
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ A library for formalization of linear error-correcting codes ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
Uses Software
Cites Work
- A Mathematical Theory of Communication
- Proofs of randomized algorithms in Coq
- Using theorem proving to verify expectation and variance for discrete random variables
- Computer-Aided Cryptographic Proofs
- Formalization of Shannon’s Theorems in SSReflect-Coq
- Three Chapters of Measure Theory in Isabelle/HOL
- Formalization of Entropy Measures in HOL
- Canonical Big Operators
- Communication Theory of Secrecy Systems*
- Fifty years of Shannon theory
- The method of types [information theory]
- Elements of Information Theory
- On the Formalization of the Lebesgue Integration Theory in HOL
- Information Theory
