Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development , Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

D. Bridges and E. Palmgren, Constructive Mathematics. The Stanford Encyclopedia of Philosophy, 2013.

D. Bridges and S. Reeves, Constructive Mathematics in Theory and Programming Practice, Philosophia Mathematica, vol.7, issue.1, 1997.
DOI : 10.1093/philmat/7.1.65

D. S. Bridges, Constructive mathematics: a foundation for computable analysis, Theoretical Computer Science, vol.219, issue.1-2, pp.95-109, 1999.
DOI : 10.1016/S0304-3975(98)00285-0

A. Chlipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, 2013.

A. Chollet, Formalismes non classiques pour le traitement informatique de la topologie et de la géométrie discrète, 2010.

A. Chollet, G. Wallet, L. Fuchs, E. Andres, and G. Largeteau-skapin, Foundational aspects of multiscale digitization, Theoretical Computer Science, vol.466, pp.2-19, 2012.
DOI : 10.1016/j.tcs.2012.07.026
URL : https://hal.archives-ouvertes.fr/hal-00857689

A. Chollet, G. Wallet, L. Fuchs, G. Largeteau-skapin, and E. Andres, Insight in discrete geometry and computational content of a discrete model of the continuum, Pattern Recognition, vol.42, issue.10, pp.2220-2228, 2009.
DOI : 10.1016/j.patcog.2008.12.005
URL : https://hal.archives-ouvertes.fr/hal-00347900

A. Chollet, G. Wallet, L. Fuchs, G. Largeteau-skapin, and E. Andres, ??-Arithmetization: A Discrete Multi-resolution Representation of Real Functions, Combinatorial Image Analysis: 13th International Workshop, pp.316-329, 2009.
DOI : 10.1007/978-3-642-10210-3_25

F. Diener and G. Reeb, Analyse Non Standard, 1989.

M. Diener, Application du calcul de Harthong-Reeb aux routines graphiques, Le Labyrinthe du Continu, pp.424-435, 1992.

J. Fleuriot, Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL, Proceedings of Automated Deduction in Geometry 2010, 2011.
DOI : 10.1007/BF02127796

J. D. Fleuriot and L. C. Paulson, A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia, Lecture Notes in Computer Science, vol.1421, pp.3-16, 1998.
DOI : 10.1007/BFb0054241

H. Geuvers, M. Niqui, B. Spitters, and F. Wiedijk, Constructive analysis, types and exact real numbers, Mathematical Structures in Computer Science, vol.17, issue.01, pp.3-36, 2007.
DOI : 10.1017/S0960129506005834

J. Harthong, Une théorie du continu, La mathématiques non standard, pp.307-329, 1989.

M. Huth and M. Ryan, Logic in Computer Science, 2004.
DOI : 10.1017/CBO9780511810275

R. Kaye, Models of Peano Arithmetic, 1991.

R. Krebbers and B. Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, 2011.
DOI : 10.2168/LMCS-9(1:1)2013

D. Laugwitz, ??-Calculus as a generalization of field extension an alternative approach to nonstandard analysis, Nonstandard Analysis -Recent developments, pp.120-133, 1983.
DOI : 10.1007/BF01187391

D. Laugwitz, Leibniz' principle and ?-calculus, Le Labyrinthe du Continu, pp.144-155, 1992.

D. Laugwitz and C. Schmieden, Eine erweiterung der infinitesimalrechnung, Mathematische Zeitschrift, vol.89, pp.1-39, 1958.

R. Lutz, La force modélisatrice des théories infinitésimales faibles, Le Labyrinthe du Continu, pp.414-423, 1992.

N. Magaud, A. Chollet, and L. Fuchs, Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective, Annals of Mathematics and Artificial Intelligence, vol.16, issue.1???4, 2010.
DOI : 10.1007/s10472-014-9434-6
URL : https://hal.archives-ouvertes.fr/hal-01066671

P. Martin-löf, Intuitionnistic Type Theory, Bibliopolis, 1984.

P. Martin-löf, Mathematics of infinity, COLOG-88 Computer Logic, pp.146-197, 1990.
DOI : 10.1007/3-540-52335-9_54

I. Moerdijk, A model for intuitionistic non-standard arithmetic, Annals of Pure and Applied Logic, vol.73, issue.1, pp.37-51, 1995.
DOI : 10.1016/0168-0072(93)E0071-U

E. Nelson, Internal set theory: A new approach to nonstandard analysis, Bulletin of the American Mathematical Society, vol.83, issue.6, pp.1165-1198, 1977.
DOI : 10.1090/S0002-9904-1977-14398-X

E. Nelson, Radically Elementary Theory, Annals of Mathematics Studies, 1987.

R. O. Connor, Certified Exact Transcendental Real Number Computation in Coq, Lecture Notes in Computer Science, vol.5170, pp.246-261, 2008.

J. Reveillès and D. Richard, Back and forth between continuous and discrete for the working computer scientist, Annals of Mathematics and Artificial Intelligence, vol.11, issue.3, pp.1-489, 1996.
DOI : 10.1007/BF02127796