4 citations · 6 across the 5 of their papers we have counts for
5 papers
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…
A Coq Formalization of Lebesgue Integration of Nonnegative Functions
Sylvie Boldo, François Clément, Florian Faissole +2
Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and…
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…
Scaling up reservoir engineering for error-correcting codes
Vincent Martin, Alain Sarlette
Error-correcting codes are usually envisioned to counter errors by operating unitary corrections depending on the projective measurement results of some syndrome observables. We he…
The Lax-Milgram Theorem. A detailed proof 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…