Skip to content
Snippets Groups Projects
user avatar
authored
Name Last commit Last update
FEM
FiniteDim
LM
Lebesgue
.gitignore
COPYING
README.md

Numerical Analysis in Coq

Formal Developments and Proofs in Coq of Numerical Analysis Problems.

Authors: Aubry, Boldo, Clément, Faissole, Leclerc, Martin, Mayero, Mouhcine

This archive includes several Coq developments:

  • Lebesgue directory is about the Lebesgue Integration of Nonnegative Functions (see paper, report, and report);

  • Lebesgue/bochner_integral directory is about the Bochner integral (see report);

  • LM directory is about the Lax–Milgram theorem (see paper, and report);

  • FiniteDim directory is about finite dimensional subspaces (see paper).

Lebesgue is compiling in Coq 8.12 to 8.15. LM and FiniteDim are compiling in Coq 8.9.