Coquelicot: a user-friendly library of real analysis for Coq (Q2018661): 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 @@
+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 / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s11786-014-0181-1
+Normal rank
@@ Property / OpenAlex ID @@
+W1975906542
@@ Property / OpenAlex ID: W1975906542 / rank @@
+Normal rank
@@ 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
@@ links / mardi / name / links / mardi / name @@
+Publication:2018661