1 citations · 2 across the 18 of their papers we have counts for
6 papers · 1 filter
A Rocq Formalization of Simplicial Lagrange Finite Elements
Sylvie Boldo, François Clément, Vincent Martin +2
Formalization of mathematics is a major topic, that includes in particular numerical analysis, towards proofs of scientific computing programs. The present study is about the finit…
A Rocq Formalization of Monomial and Graded Orders
Sylvie Boldo, François Clément, Vincent Martin +1
Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the fi…
Finite element method. 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 for the resolution of Partial Differential Equations (PDEs), one has to formalize the mathematic…
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 the Bochner integral
Sylvie Boldo, François Clément, Louise Leclerc
The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formaliz…
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…