Formalization of Entropy Measures in HOL

DOI10.1007/978-3-642-22863-6_18zbMath1342.68295OpenAlexW162339537MaRDI QIDQ3088009

Osman Hasan, Tarek Mhamdi, Sofiène Tahar

Publication date: 17 August 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_18

Mathematics Subject Classification ID

Measures of information, entropy (94A17)

Related Items (max. 100)

A formally verified proof of the central limit theorem ⋮ Formal probabilistic analysis of detection properties in wireless sensor networks ⋮ Formal reasoning about finite-state discrete-time Markov chains in HOL ⋮ Evaluation of anonymity and confidentiality protocols using theorem proving ⋮ Formalization of Normal Random Variables in HOL ⋮ Formalization of Shannon's theorems

Uses Software

• Isabelle
• ML
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A Mathematical Theory of Communication
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Isabelle. A generic theorem prover
• Assessing security threats of looping constructs
• On the Formalization of the Lebesgue Integration Theory in HOL

This page was built for publication: Formalization of Entropy Measures in HOL