Formalization of real analysis: a survey of proof assistants and libraries
From MaRDI portal
Publication:2973239
DOI10.1017/S0960129514000437zbMATH Open1364.68327MaRDI QIDQ2973239FDOQ2973239
Catherine Lelay, Sylvie Boldo, Guillaume Melquiond
Publication date: 3 April 2017
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Recommendations
Cites Work
- A Brief Overview of Mizar
- Dense sphere packings. A blueprint for formal proofs
- Verified Real Number Calculations: A Library for Interval Arithmetic
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Partial functions in ACL2
- A comparison of Mizar and Isar
- Formalization of Bernstein polynomials and applications to global optimization
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- HOL Light: An Overview
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Towards Self-verification of HOL Light
- The HOL Light theory of Euclidean space
- Three Chapters of Measure Theory in Isabelle/HOL
- On the Formalization of the Lebesgue Integration Theory in HOL
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Certified Exact Transcendental Real Number Computation in Coq
- Title not available (Why is that?)
- Nonstandard analysis in ACL2
- A computer-verified monadic functional implementation of the integral
- Packaging Mathematical Structures
- Provably correct conflict prevention bands algorithms
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Constructing the real numbers in HOL
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- The Picard Algorithm for Ordinary Differential Equations in Coq
- A certified, corecursive implementation of exact real numbers
- Verifying Mixed Real-Integer Quantifier Elimination
- Automatic Differentiation in ACL2
- Semi-Automated Mathematics
- A monadic, functional implementation of real numbers
- Real Number Calculations and Theorem Proving
- Non-uniform (hyper/multi)coherence spaces
- Formal Verification of Exact Computations Using Newton’s Method
- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure
Cited In (30)
- Integral of continuous functions of two variables
- Multidimensional measure space and integration
- Implicit definitions with differential equations for KeYmaera X (system description)
- A Coq formalization of Lebesgue integration of nonnegative functions
- Title not available (Why is that?)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Summable family in a commutative group
- Some representations of real numbers using integer sequences
- Groups -- additive notation.
- The flow of ODEs: formalization of variational equation and Poincaré map
- Verified Real Asymptotics in Isabelle/HOL
- Accurate calculation of Euclidean norms using double-word arithmetic
- Using theory interpretation to mechanise the reals in a theorem prover
- Banishing Ultrafilters from Our Consciousness
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- Axiomatic reals and certified efficient exact real computation
- Formalization of functional variation in HOL Light
- Integral of continuous three variable functions
- Formalization of the integral calculus in the PVS theorem prover
- A formally verified proof of the central limit theorem
- Title not available (Why is that?)
- Title not available (Why is that?)
- Iscalc: An Interactive Symbolic Computation Framework (System Description)
- A Coq formalization of Lebesgue induction principle and Tonelli's theorem
- Title not available (Why is that?)
- Gauge integral
- Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
- Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”
- Coquelicot: a user-friendly library of real analysis for Coq
- Differentiation on interval
Uses Software
This page was built for publication: Formalization of real analysis: a survey of proof assistants and libraries
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2973239)
