Formalization of real analysis: a survey of proof assistants and libraries (Q2973239): Difference between revisions

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