1 citations · 2 across the 3 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2022
Lebesgue Induction and Tonelli's Theorem in Coq
Sylvie Boldo, François Clément, Vincent Martin +2
Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assista…
cs.LO2021★ 1 cited
Lebesgue integration. Detailed proofs to be formalized in Coq
François Clément, Vincent Martin
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and result…