A Coq Formal Proof of the Lax–Milgram theorem

Abstract : The Finite Element Method is a widely-used method to solve numerical problems coming for instance from physics or biology. 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 results that allow to establish the sound-ness of the method. The Lax–Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. This article presents the full formal proof of the Lax–Milgram theorem in Coq. It requires many results from linear algebra, geometry, functional analysis , and Hilbert spaces.
Type de document :
Communication dans un congrès
6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. <http://cpp2017.mpi-sws.org/>
Liste complète des métadonnées

https://hal.inria.fr/hal-01391578
Contributeur : Sylvie Boldo <>
Soumis le : jeudi 3 novembre 2016 - 15:10:25
Dernière modification le : vendredi 17 février 2017 - 16:10:41
Document(s) archivé(s) le : samedi 4 février 2017 - 14:07:29

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01391578, version 1

Citation

Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. A Coq Formal Proof of the Lax–Milgram theorem. 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. <http://cpp2017.mpi-sws.org/>. <hal-01391578>

Partager

Métriques

Consultations de
la notice

465

Téléchargements du document

243