Coquelicot: a user-friendly library of real analysis for Coq (Q2018661): Difference between revisions

@@ Property / cites work @@
+A monadic, functional implementation of real numbers
+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
@@ Property / cites work @@
+Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
+Normal rank
@@ Property / cites work @@
+Wave equation numerical resolution: a comprehensive mechanized proof of a C program
+Normal rank
@@ Property / cites work @@
+Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
+Normal rank
@@ Property / cites work @@
+Formalization of real analysis: a survey of proof assistants and libraries
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435465
@@ Property / cites work: Q4435465 / rank @@
+Normal rank
@@ Property / cites work @@
+Verified Real Number Calculations: A Library for Interval Arithmetic
+Normal rank
@@ Property / cites work @@
+Q2754041
@@ Property / cites work: Q2754041 / rank @@
+Normal rank
@@ Property / cites work @@
+Nonstandard analysis in ACL2
@@ Property / cites work: Nonstandard analysis in ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736391
@@ Property / cites work: Q4736391 / 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 @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / rank @@
+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 @@
+Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Q3184782
@@ Property / cites work: Q3184782 / rank @@
+Normal rank
@@ Property / cites work @@
+Type classes for efficient exact real arithmetic in Coq
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Bounds on Real-Valued Functions with Computations
+Normal rank
@@ Property / cites work @@
+Formalization of Bernstein polynomials and applications to global optimization
+Normal rank
@@ Property / cites work @@
+A Brief Overview of Mizar
@@ Property / cites work: A Brief Overview of Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+A computer-verified monadic functional implementation of the integral
+Normal rank