70 citations · 91 across the 10 of their papers we have counts for
8 papers · 1 filter
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…
Teaching Divisibility and Binomials with Coq
Sylvie Boldo, François Clément, David Hamelin +2
The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely ta…
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…
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…
Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
Sylvie Boldo, Francois Clement, Jean-Christophe Filliâtre +3
We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors…