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

DOI10.1007/s10472-014-9434-6zbMath1326.03074OpenAlexW1999892388MaRDI 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 geometryformal proofsCoqexact computationsarithmetisation schemenon-standard arithmetic

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Nonstandard models of arithmetic (03H15) Intuitionistic mathematics (03F55)

Related Items (6)

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

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

This page was built for publication: Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective