Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective (Q2354911): Difference between revisions

@@ 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/s10472-014-9434-6
+Normal rank
@@ Property / OpenAlex ID @@
+W1999892388
@@ Property / OpenAlex ID: W1999892388 / rank @@
+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 @@
+Q4249889
@@ Property / cites work: Q4249889 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive Mathematics in Theory and Programming Practice
+Normal rank
@@ Property / cites work @@
+Constructive mathematics: a foundation for computable analysis
+Normal rank
@@ Property / cites work @@
+Q5417200
@@ Property / cites work: Q5417200 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive analysis, types and exact real numbers
+Normal rank
@@ Property / cites work @@
+Foundational aspects of multiscale digitization
@@ Property / cites work: Foundational aspects of multiscale digitization / rank @@
+Normal rank
@@ Property / cites work @@
+Insight in discrete geometry and computational content of a discrete model of the continuum
+Normal rank
@@ Property / cites work @@
+Ω-Arithmetization: A Discrete Multi-resolution Representation of Real Functions
+Normal rank
@@ Property / cites work @@
+Q3993282
@@ Property / cites work: Q3993282 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4037536
@@ Property / cites work: Q4037536 / rank @@
+Normal rank
@@ Property / cites work @@
+Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Q3141106
@@ Property / cites work: Q3141106 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic in Computer Science
@@ Property / cites work: Logic in Computer Science / rank @@
+Normal rank
@@ Property / cites work @@
+Q4001935
@@ Property / cites work: Q4001935 / rank @@
+Normal rank
@@ Property / cites work @@
+Type classes for efficient exact real arithmetic in Coq
+Normal rank
@@ Property / cites work @@
+Q4749840
@@ Property / cites work: Q4749840 / rank @@
+Normal rank
@@ Property / cites work @@
+Eine Erweiterung der Infinitesimalrechnung
@@ Property / cites work: Eine Erweiterung der Infinitesimalrechnung / rank @@
+Normal rank
@@ Property / cites work @@
+Q4037535
@@ Property / cites work: Q4037535 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
+Normal rank
@@ Property / cites work @@
+Q5752569
@@ Property / cites work: Q5752569 / rank @@
+Normal rank
@@ Property / cites work @@
+A model for intuitionistic non-standard arithmetic
+Normal rank
@@ Property / cites work @@
+Internal set theory: A new approach to nonstandard analysis
+Normal rank
@@ Property / cites work @@
+Radically Elementary Probability Theory. (AM-117)
@@ Property / cites work: Radically Elementary Probability Theory. (AM-117) / rank @@
+Normal rank
@@ Property / cites work @@
+Certified Exact Transcendental Real Number Computation in Coq
+Normal rank
@@ Property / cites work @@
+Back and forth between continuous and discrete for the working computer scientist
+Normal rank