Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective

DOI10.1007/s10472-014-9434-6zbMath1326.03074MaRDI QIDQ2354911

Laurent Fuchs, Nicolas Magaud, Agathe Chollet

Publication date: 27 July 2015

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-014-9434-6

zbMATH Keywords

discrete geometry; formal proofs; Coq; exact computations; arithmetisation scheme; non-standard arithmetic

Mathematics Subject Classification ID

03F60: Constructive and recursive analysis

03H15: Nonstandard models of arithmetic

03F55: Intuitionistic mathematics

Related Items

Some representations of real numbers using integer sequences, Foundational aspects of multiscale digitization, Formalization of the Poincaré disc model of hyperbolic geometry, Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective, Multi-scale arithmetization of linear transformations, Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL

Uses Software

• Coq

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Eine Erweiterung der Infinitesimalrechnung
• Insight in discrete geometry and computational content of a discrete model of the continuum
• Constructive mathematics: a foundation for computable analysis
• Back and forth between continuous and discrete for the working computer scientist
• A model for intuitionistic non-standard arithmetic
• Foundational aspects of multiscale digitization
• Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
• Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL
• Constructive analysis, types and exact real numbers
• Certified Exact Transcendental Real Number Computation in Coq
• Ω-Arithmetization: A Discrete Multi-resolution Representation of Real Functions
• Radically Elementary Probability Theory. (AM-117)
• Internal set theory: A new approach to nonstandard analysis
• Constructive Mathematics in Theory and Programming Practice
• Logic in Computer Science
• Type classes for efficient exact real arithmetic in Coq
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item