Formalization of entropy measures in HOL

DOI10.1007/978-3-642-22863-6_18MaRDI QIDQ3088009zbMATH OpenOpenAlexFDO

Authors Tarek Mhamdi, Osman Hasan, 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)

Recommendations

• Formal analysis of information flow in HOL
• Formalization of Shannon's theorems in SSReflect-Coq
• Formal Analysis of Information Flow Using Min-Entropy and Belief Min-Entropy
• Formalization of Shannon's theorems
• Reasoning about conditional probabilities in a higher-order-logic theorem prover

Cites work

• A Mathematical Theory of Communication
• Assessing security threats of looping constructs
• scientific article; zbMATH DE number 3890413 (Why is no real title available?)
• scientific article; zbMATH DE number 107482 (Why is no real title available?)
• scientific article; zbMATH DE number 3542687 (Why is no real title available?)
• scientific article; zbMATH DE number 2090929 (Why is no real title available?)
• scientific article; zbMATH DE number 2090930 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Isabelle. A generic theorem prover
• On the formalization of the Lebesgue integration theory in HOL
• Probabilistic guarded commands mechanized in HOL
• The dining cryptographers problem: Unconditional sender and recipient untraceability

Cited in

(10)

• A formally verified proof of the central limit theorem
• Formalization of Shannon's theorems
• Formal reasoning about finite-state discrete-time Markov chains in HOL
• Formalization of normal random variables in HOL
• Formalization of Shannon's theorems in SSReflect-Coq
• Formal analysis of information flow in HOL
• Evaluation of anonymity and confidentiality protocols using theorem proving
• Formal Verification of Rewriting Rules for Dynamic Fault Trees
• Dynamic dependability analysis of shuffle-exchange networks
• Formal probabilistic analysis of detection properties in wireless sensor networks

Describes a project that uses

Uses Software

• HOL
• Isabelle
• ML

This page was built for publication: Formalization of entropy measures in HOL

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