ITP 2010 - PDF Preprint Papers

ITP 2010 Interactive Theorem Proving

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed ITP-2010 Paper

click to vote

ITP
2010

230views Mathematics» more ITP 2010»

On the Formalization of the Lebesgue Integration Theory in HOL

14 years 1 months ago

Download hvg.ece.concordia.ca

Lebesgue integration is a fundamental concept in many mathematical theories, such as real analysis, probability and information theory. Reported higher-order-logic formalizations o...

Tarek Mhamdi, Osman Hasan, Sofiène Tahar

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	230	On the Formalization of the Lebesgue Integration Theory in HOL	claim
2	179	The Isabelle Collections Framework	claim
3	178	Developing the Algebraic Hierarchy with Type Classes in Coq	claim
4	178	Interactive Termination Proofs Using Termination Cores	claim
5	172	Equations: A Dependent Pattern-Matching Compiler	claim
6	172	Automated Machine-Checked Hybrid System Safety Proofs	claim
7	165	A Mechanized Translation from Higher-Order Logic to Set Theory	claim
8	164	Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder	claim
9	163	Fast LCF-Style Proof Reconstruction for Z3	claim
10	161	Separation Logic Adapted for Proofs by Rewriting	claim
11	159	Programming Language Techniques for Cryptographic Proofs	claim
12	156	The Optimal Fixed Point Combinator	claim
13	155	A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture	claim
14	155	Translation in XBRL standardization	claim
15	152	Higher-Order Abstract Syntax in Isabelle/HOL	claim
16	150	Coverset Induction with Partiality and Subsorts: A Powerlist Case Study	claim
17	149	A Framework for Formal Verification of Compiler Optimizations	claim
18	148	A Mechanically Verified AIG-to-BDD Conversion Algorithm	claim
19	143	Formal Study of Plane Delaunay Triangulation	claim
20	143	A Certified Denotational Abstract Interpreter	claim
21	142	Inductive Consequences in the Calculus of Constructions	claim
22	141	(Nominal) Unification by Recursive Descent with Triangular Substitutions	claim
23	140	Case-Analysis for Rippling and Inductive Proof	claim
24	139	Validating QBF Invalidity in HOL4	claim
25	138	An Efficient Coq Tactic for Deciding Kleene Algebras	claim
26	137	Importing HOL Light into Coq	claim
27	132	Extending Coq with Imperative Features and Its Application to SAT Verification	claim
28	129	Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure	claim
29	126	A Formally Verified OS Kernel. Now What?	claim
30	119	Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison	claim
31	118	Formal Proof of a Wave Equation Resolution Scheme: The Method Error	claim
32	114	A New Foundation for Nominal Isabelle	claim
33	109	A Tactic Language for Declarative Proofs	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers