Skip to content
Snippets Groups Projects
Select Git revision
  • 5de5a67a5f483ca3f57ec85c05ce1858f112800b
  • master default protected
  • Subset
  • 2.1
  • FE_new_def
  • 2.0 protected
  • 1.0 protected
  • 2.0.0 protected
  • PhD_HM_2024
  • 1.0 protected
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
13 results

rocq-num-analysis

Name Last commit Last update
FEM
FiniteDim
LM
Lebesgue
.gitignore
COPYING
README.md
opam
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, paper, and report);

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

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

Opam package coq-num-analysis: version 1.0 provides Lebesgue, and LM.

Lebesgue and LM are compiling in Coq 8.12 to 8.16.