Formalization of real analysis: a survey of proof assistants and libraries

DOI10.1017/S0960129514000437zbMath1364.68327MaRDI QIDQ2973239

Catherine Lelay, Sylvie Boldo, Guillaume Melquiond

Publication date: 3 April 2017

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Related Items (19)

Summable family in a commutative group ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Axiomatic reals and certified efficient exact real computation ⋮ Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic” ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Unnamed Item ⋮ Differentiation on interval ⋮ Gauge integral ⋮ Formalization of functional variation in HOL Light ⋮ A formally verified proof of the central limit theorem ⋮ A Coq formalization of Lebesgue induction principle and Tonelli's theorem ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ Groups -- additive notation. ⋮ Banishing Ultrafilters from Our Consciousness ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ Formalization of Euler-Lagrange equation set based on variational calculus in HOL light ⋮ Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers ⋮ Implicit definitions with differential equations for KeYmaera X (system description) ⋮ Some representations of real numbers using integer sequences

Uses Software

• ACL2
• Coq
• Isabelle/HOL
• PVS
• Mizar
• ProofPower
• HOL Light
• C-CoRN

Cites Work

• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Provably correct conflict prevention bands algorithms
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A certified, corecursive implementation of exact real numbers
• A computer-verified monadic functional implementation of the integral
• Constructing the real numbers in HOL
• Partial functions in ACL2
• A comparison of Mizar and Isar
• The HOL Light theory of Euclidean space
• Formalization of Bernstein polynomials and applications to global optimization
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Non-uniform (hyper/multi)coherence spaces
• Three Chapters of Measure Theory in Isabelle/HOL
• On the Generation of Positivstellensatz Witnesses in Degenerate Cases
• Automatic Differentiation in ACL2
• HOL Light: An Overview
• A Brief Overview of Mizar
• Packaging Mathematical Structures
• Formal Verification of Exact Computations Using Newton’s Method
• A monadic, functional implementation of real numbers
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Real Number Calculations and Theorem Proving
• Certified Exact Transcendental Real Number Computation in Coq
• Towards Self-verification of HOL Light
• Verifying Mixed Real-Integer Quantifier Elimination
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Semi-Automated Mathematics
• Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure
• On the Formalization of the Lebesgue Integration Theory in HOL
• Nonstandard analysis in ACL2

This page was built for publication: Formalization of real analysis: a survey of proof assistants and libraries