Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
From MaRDI portal
Publication:4916067
DOI10.1007/978-3-642-35308-6_22zbMath1383.68070OpenAlexW112168304MaRDI QIDQ4916067
Sylvie Boldo, Guillaume Melquiond, Catherine Lelay
Publication date: 19 April 2013
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-35308-6_22
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Differentiation on interval ⋮ A formally verified proof of the central limit theorem ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ Polynomial function intervals for floating-point software verification ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ Theorem-proving analysis of digital control logic interacting with continuous dynamics
Uses Software
This page was built for publication: Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
