Formalization of real analysis: a survey of proof assistants and libraries
From MaRDI portal
(Redirected from Publication:2973239)
Recommendations
Cites work
- scientific article; zbMATH DE number 1259143 (Why is no real title available?)
- A Brief Overview of Mizar
- A certified, corecursive implementation of exact real numbers
- A comparison of Mizar and Isar
- A computer-verified monadic functional implementation of the integral
- A monadic, functional implementation of real numbers
- Automatic differentiation in ACL2
- Certified Exact Transcendental Real Number Computation in Coq
- Constructing the real numbers in HOL
- Dense sphere packings. A blueprint for formal proofs
- Formal Verification of Exact Computations Using Newton’s Method
- Formalization of Bernstein polynomials and applications to global optimization
- HOL Light: An Overview
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Non-uniform (hyper/multi)coherence spaces
- Nonstandard analysis in ACL2
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- On the formalization of the Lebesgue integration theory in HOL
- Packaging Mathematical Structures
- Partial functions in ACL2
- Provably correct conflict prevention bands algorithms
- Real Number Calculations and Theorem Proving
- Semi-Automated Mathematics
- The HOL Light theory of Euclidean space
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Three chapters of measure theory in Isabelle/HOL
- Towards Self-verification of HOL Light
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Using a first order logic to verify that some set of reals has no Lebesgue measure
- Verified Real Number Calculations: A Library for Interval Arithmetic
- Verifying Mixed Real-Integer Quantifier Elimination
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
Cited in
(40)- Differentiation on interval
- Banishing ultrafilters from our consciousness
- Integral of continuous functions of two variables
- Multidimensional measure space and integration
- Implicit definitions with differential equations for KeYmaera X (system description)
- A formalization of properties of continuous functions on closed intervals
- A Coq formalization of Lebesgue integration of nonnegative functions
- Elements of mathematical analysis in PVS
- Summable family in a commutative group
- scientific article; zbMATH DE number 1951639 (Why is no real title available?)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Computable analysis and notions of continuity in \textsc{Coq}
- Switched systems in Coq for modeling periodic controllers
- Groups -- additive notation.
- The flow of ODEs: formalization of variational equation and Poincaré map
- Some representations of real numbers using integer sequences
- Verified Real Asymptotics in Isabelle/HOL
- Using theory interpretation to mechanise the reals in a theorem prover
- Accurate calculation of Euclidean norms using double-word arithmetic
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- The interval domain in homotopy type theory
- Axiomatic reals and certified efficient exact real computation
- Computable analysis for verified exact real computation
- Formalization of functional variation in HOL Light
- Formalization of the integral calculus in the PVS theorem prover
- Integral of continuous three variable functions
- A formally verified proof of the central limit theorem
- scientific article; zbMATH DE number 1670741 (Why is no real title available?)
- scientific article; zbMATH DE number 1927426 (Why is no real title available?)
- Iscalc: An Interactive Symbolic Computation Framework (System Description)
- Formalization techniques for asymptotic reasoning in classical analysis
- Gauge integral
- A Coq formalization of Lebesgue induction principle and Tonelli's theorem
- Formalization of convergence rates of four first-order algorithms for convex optimization
- The HOL Light theory of Euclidean space
- Extracting efficient exact real number computation from proofs in constructive type theory
- Coquelicot: a user-friendly library of real analysis for Coq
- Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”
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)
