On the Formalization of the Lebesgue Integration Theory in HOL
From MaRDI portal
Publication:5747663
DOI10.1007/978-3-642-14052-5_27zbMath1291.68362OpenAlexW1814275833MaRDI QIDQ5747663
Tarek Mhamdi, Osman Hasan, Sofiène Tahar
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_27
Related Items
The gauge integral theory in HOL4, Towards Formal Fault Tree Analysis Using Theorem Proving, Formalization of reliability block diagrams in higher-order logic, Program logic for higher-order probabilistic programs in Isabelle/HOL, An approach for lifetime reliability analysis using theorem proving, A Coq formalization of Lebesgue integration of nonnegative functions, Measure construction by extension in dependent type theory with application to integration, Formal probabilistic analysis of detection properties in wireless sensor networks, Formalization of real analysis: a survey of proof assistants and libraries, Evaluation of anonymity and confidentiality protocols using theorem proving, Formalization of Normal Random Variables in HOL, Formal Dependability Modeling and Analysis: A Survey, Three Chapters of Measure Theory in Isabelle/HOL, Formalization of Entropy Measures in HOL, Verified interactive computation of definite integrals, Towards the Formal Reliability Analysis of Oil and Gas Pipelines, Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation, Formalization of Shannon's theorems, On the formalization of gamma function in HOL
Uses Software
