Cover Image

Finite element method. Detailed proofs to be formalized in Coq

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Clément, François, Martin, Vincent
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Numerical Analysis
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Teaching Divisibility and Binomials with Coq
by: Boldo, Sylvie, et al.
Published: (2024)

Transient Evaluation of Non-Markovian Models by Stochastic State Classes and Simulation
by: Dengler, Gabriel, et al.
Published: (2024)

Automatic Verification of Floating-Point Accumulation Networks
by: Zhang, David K., et al.
Published: (2025)

Time-Sensitive Importance Splitting
by: Dengler, Gabriel, et al.
Published: (2025)

Shock with Confidence: Formal Proofs of Correctness for Hyperbolic Partial Differential Equation Solvers
by: Gorard, Jonathan, et al.
Published: (2025)

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
by: Tao, Yichen, et al.
Published: (2026)

Numerical Considerations in Weighted Model Counting
by: Bryant, Randal E.
Published: (2025)

Bean: A Language for Backward Error Analysis
by: Kellison, Ariel E., et al.
Published: (2025)

A Rocq Formalization of Simplicial Lagrange Finite Elements
by: Boldo, Sylvie, et al.
Published: (2026)

CoqPilot, a plugin for LLM-based generation of proofs
by: Kozyrev, Andrei, et al.
Published: (2024)

A Rocq Formalization of Monomial and Graded Orders
by: Boldo, Sylvie, et al.
Published: (2025)

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
by: Affeldt, Reynald, et al.
Published: (2024)

Maths with Coq in L1, a pedagogical experiment
by: Kerjean, Marie, et al.
Published: (2025)

Towards solid abelian groups: A formal proof of Nöbeling's theorem
by: Asgeirsson, Dagur
Published: (2023)

A Coq Formalization of Unification Modulo Exclusive-Or
by: Xu, Yichi, et al.
Published: (2025)

A tensor network formalism for neuro-symbolic AI
by: Goessmann, Alex, et al.
Published: (2026)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

A beginner guide to Iris, Coq and separation logic
by: Dietrich, Elizabeth
Published: (2021)

Towards Automatic Transformations of Coq Proof Scripts
by: Magaud, Nicolas
Published: (2024)

A proof theory of (omega-)context-free languages, via non-wellfounded proofs
by: Das, Anupam, et al.
Published: (2024)

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
by: Soldevila, Mallku, et al.
Published: (2024)

A proof-theoretic approach to abstract interpretation
by: D'Silva, Vijay, et al.
Published: (2026)

Bijective proofs for Eulerian numbers of types B and D
by: Santocanale, Luigi
Published: (2021)

Comparative study of different quadrature methods for cut elements
by: Loibl, Michael, et al.
Published: (2026)

A logic of judgmental existence and its relation to proof irrelevance
by: Pezlar, Ivo
Published: (2024)

The proof theory and semantics of second-order (intuitionistic) tense logic
by: Becker, Justus, et al.
Published: (2026)

A coupled finite element-virtual element method for thermomechanical analysis of electronic packaging structures
by: Gong, Yanpeng, et al.
Published: (2025)

A method for the automated generation of proof exercises with comparable levels of proving complexity
by: Mendes, João, et al.
Published: (2026)

Incompleteness for stably computable formal systems
by: Savelyev, Yasha
Published: (2022)

A linear proof language for second-order intuitionistic linear logic
by: Díaz-Caro, Alejandro, et al.
Published: (2023)

Wider systems for linear logic with fixed points: proof theory and complexity
by: Das, Anupam, et al.
Published: (2026)

A finite element method for anisotropic crystal growth on surfaces
by: Garcke, Harald, et al.
Published: (2024)

Taming Differentiable Logics with Coq Formalisation
by: Affeldt, Reynald, et al.
Published: (2024)

The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
by: Oda, Yukihiro, et al.
Published: (2021)

Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
by: Florath, Andreas
Published: (2024)

Sparsity comparison of polytopal finite element methods
by: Lehrenfeld, Christoph, et al.
Published: (2024)

Efficient Solving of Quantified Inequality Constraints over the Real Numbers
by: Ratschan, Stefan
Published: (2002)

Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)
by: Appel, Andrew W.
Published: (2025)

A Coq-based Axiomatization of Tarski's Mereogeometry
by: Barlatier, Patrick, et al.
Published: (2025)

Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss
by: Kozhemiachenko, Daniil
Published: (2024)