Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
From MaRDI portal
Publication:2354911
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
discrete geometry; formal proofs; Coq; exact computations; arithmetisation scheme; non-standard arithmetic
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
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