{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T10:03:08Z","timestamp":1771063388956,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2014,10,17]],"date-time":"2014-10-17T00:00:00Z","timestamp":1413504000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10472-014-9434-6","type":"journal-article","created":{"date-parts":[[2014,10,16]],"date-time":"2014-10-16T01:13:56Z","timestamp":1413422036000},"page":"309-332","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective"],"prefix":"10.1007","volume":"74","author":[{"given":"Nicolas","family":"Magaud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agathe","family":"Chollet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Fuchs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,17]]},"reference":[{"key":"9434_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Berlin Heidelberg New York (2004)"},{"key":"9434_CR2","unstructured":"Bridges, D., Palmgren, E.: Constructive Mathematics. The Stanford Encyclopedia of Philosophy. available from http:\/\/plato.stanford.edu\/archives\/win2013\/entries\/mathematics-constructive\/ (2013)"},{"key":"9434_CR3","unstructured":"Bridges, D., Reeves, S.: Constructive mathematics, in theory and programming practice. Technical Report CDMTCS-068, Centre for Discrete Mathematics and Theorical Computer Science (1997)"},{"issue":"1\u20132","key":"9434_CR4","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/S0304-3975(98)00285-0","volume":"219","author":"DS Bridges","year":"1999","unstructured":"Bridges, D.S.: Constructive mathematics: A foundation for computable analysis. Theor. Comput. Sci. 219 (1\u20132), 95\u2013109 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"9434_CR5","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified programming with dependent types: A pragmatic introduction to the coq proof assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified programming with dependent types: A pragmatic introduction to the coq proof assistant. MIT Press, Cambridge (2013)"},{"key":"9434_CR6","unstructured":"Chollet, A.: Formalismes non classiques pour le traitement informatique de la topologie et de la g\u00e9om\u00e9trie discr\u00e8te. PhD thesis, Universit\u00e9 de la Rochelle (2010)"},{"key":"9434_CR7","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.tcs.2012.07.026","volume":"466","author":"A Chollet","year":"2012","unstructured":"Chollet, A., Wallet, G., Fuchs, L., Andres, E., Largeteau-Skapin, G.: Foundational aspects of multiscale digitization. Theor. Comput. Sci. 466, 2\u201319 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"9434_CR8","doi-asserted-by":"crossref","first-page":"2220","DOI":"10.1016\/j.patcog.2008.12.005","volume":"42","author":"A Chollet","year":"2009","unstructured":"Chollet, A., Wallet, G., Fuchs, L., Largeteau-Skapin, G., Andres, E.: Insight in discrete geometry and computational content of a discrete model of the continuum. Pattern Recog. 42, 2220\u20132228 (2009)","journal-title":"Pattern Recog."},{"key":"9434_CR9","doi-asserted-by":"crossref","unstructured":"Chollet, A., Wallet, G., Fuchs, L., Largeteau-Skapin, G., Andres, E.: \u03a9-Arithmetization: A Discrete Multi-resolution Representation of Real Functions. In: Wiederhold, P., Barneva, P.R. (eds.) Combinatorial Image Analysis: 13th International Workshop, IWCIA of Lecture Notes in Computer Science (LNCS), vol. 5852, pp 316\u2013329, Mexico (2009)","DOI":"10.1007\/978-3-642-10210-3_25"},{"key":"9434_CR10","unstructured":"Coq development team: The Coq Proof Assistant Reference Manual, Version 8.2. LogiCal Project (2008)"},{"key":"9434_CR11","volume-title":"Analyse non standard","author":"F Diener","year":"1989","unstructured":"Diener, F., Reeb, G.: Analyse non standard. Hermann, Paris (1989)"},{"key":"9434_CR12","first-page":"424","volume-title":"Le Labyrinthe du Continu","author":"M Diener","year":"1992","unstructured":"Diener, M.: Application du calcul de Harthong-Reeb aux routines graphiques. In: Salanskis, J.-M., Sinaceurs, H. (eds.) Le Labyrinthe du Continu, pp 424\u2013435. Springer, Berlin Heidelberg New York (1992)"},{"key":"9434_CR13","volume-title":"Proceedings of Automated Deduction in Geometry 2010 of LNAI, vol 6877","author":"J Fleuriot","year":"2011","unstructured":"Fleuriot, J.: Exploring the foundations of discrete analytical geometry in Isabelle\/HOL. In: Schreck, P., Richter-Gebert, J., Narboux, J. (eds.) Proceedings of Automated Deduction in Geometry 2010 of LNAI, vol. 6877. Springer, Berlin Heidelberg New York (2011)"},{"key":"9434_CR14","first-page":"3","volume-title":"CADE of Lecture Notes in Computer Science, vol. 1421","author":"JD Fleuriot","year":"1998","unstructured":"Fleuriot, J.D., Paulson, L.C.: A combination of nonstandard analysis and geometry theorem proving, with application to newton\u2019s principia. In: Kirchner, C., Kirchner, H. (eds.) CADE of Lecture Notes in Computer Science, vol. 1421, pp 3\u201316. Springer, Berlin Heidelberg New York (1998)"},{"issue":"1","key":"9434_CR15","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S0960129506005834","volume":"17","author":"H Geuvers","year":"2007","unstructured":"Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1), 3\u201336 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9434_CR16","unstructured":"Harthong, J.: Une th\u00e9orie du continu. In: Barreau, H., Harthong, J. (eds.) La math\u00e9matiques non standard, pp 307\u2013329, Paris (1989). \u00c9ditions du CNRS"},{"key":"9434_CR17","doi-asserted-by":"crossref","unstructured":"Huth, M., Ryan, M., 2nd ed: Logic in Computer Science. Cambridge University Press (2004)","DOI":"10.1017\/CBO9780511810275"},{"key":"9434_CR18","doi-asserted-by":"crossref","unstructured":"Kaye, R.: Models of Peano Arithmetic. Oxford Science Publications (1991)","DOI":"10.1093\/oso\/9780198532132.001.0001"},{"key":"9434_CR19","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Meth. Comput. Sci. 9(1) (2011)","DOI":"10.2168\/LMCS-9(1:1)2013"},{"key":"9434_CR20","doi-asserted-by":"crossref","unstructured":"Laugwitz, D.: \u03a9-calculus as a generalization of field extension an alternative approach to nonstandard analysis. In: Hurd, A. (ed.) Nonstandard Analysis - Recent developments, volume 983 of Lecture Notes in Mathematics, pp 120\u2013133. Springer (1983)","DOI":"10.1007\/BFb0065337"},{"key":"9434_CR21","first-page":"144","volume-title":"Le Labyrinthe du Continu","author":"D Laugwitz","year":"1992","unstructured":"Laugwitz, D.: Leibniz\u2019 principle and \u03a9-calculus. In: Salanskis, J., Sinacoeur, H. (eds.) Le Labyrinthe du Continu, pp 144\u2013155. Springer, France (1992)"},{"key":"9434_CR22","first-page":"1","volume":"89","author":"D Laugwitz","year":"1958","unstructured":"Laugwitz, D., Schmieden, C.: Eine erweiterung der infinitesimalrechnung. Mathematische Zeitschrift 89, 1\u201339 (1958)","journal-title":"Mathematische Zeitschrift"},{"key":"9434_CR23","unstructured":"Lutz, R.: La force mod\u00e9lisatrice des th\u00e9ories infinit\u00e9simales faibles. In: Salanskis, J.-M., Sinaceur, H. (eds.) Le Labyrinthe du Continu, pp 414\u2013423. Springer-Verlag (1992)"},{"key":"9434_CR24","unstructured":"Magaud, N., Chollet, A., Fuchs, L.: Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective. In: ADG\u20192010 (2010). Accepted for presentation at the conference"},{"key":"9434_CR25","volume-title":"Intuitionnistic Type Theory","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P.: Intuitionnistic Type Theory. Bibliopolis, Napoli (1984)"},{"key":"9434_CR26","first-page":"146","volume-title":"Mathematics of infinity. In: COLOG-88 Computer Logic, Lecture Notes in Computer Science","author":"P Martin-L\u00f6f","year":"1990","unstructured":"Martin-L\u00f6f, P.: Mathematics of infinity. In: COLOG-88 Computer Logic, Lecture Notes in Computer Science, pp 146\u2013197. Springer-Verlag , Berlin (1990)"},{"issue":"1","key":"9434_CR27","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0168-0072(93)E0071-U","volume":"73","author":"I Moerdijk","year":"1995","unstructured":"Moerdijk, I.: A model for intuitionistic non-standard arithmetic. Ann. Pure Appl. Logic 73(1), 37\u201351 (1995)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"6","key":"9434_CR28","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1090\/S0002-9904-1977-14398-X","volume":"83","author":"E Nelson","year":"1977","unstructured":"Nelson, E.: Internal set theory: A new approach to nonstandard analysis. Bull. Am. Math. Soc. 83(6), 1165\u20131198 (1977)","journal-title":"Bull. Am. Math. Soc."},{"key":"9434_CR29","unstructured":"Nelson, E.: Radically Elementary Theory. Annals of Mathematics Studies. Princeton University Press (1987)"},{"key":"9434_CR30","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, R.: Certified exact transcendental real number computation in Coq. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs, volume 5170 of Lecture Notes in Computer Science, pp 246\u2013261. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_21"},{"issue":"1\u20134","key":"9434_CR31","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF02127796","volume":"16","author":"J-P Reveill\u00e8s","year":"1996","unstructured":"Reveill\u00e8s, J.-P., Richard, D.: Back and forth between continuous and discrete for the working computer scientist. Ann. Math. Artif. Intell., Math. Inform. 16(1\u20134), 89\u2013152 (1996)","journal-title":"Ann. Math. Artif. Intell., Math. Inform."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9434-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-014-9434-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9434-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T23:27:59Z","timestamp":1717457279000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-014-9434-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,17]]},"references-count":31,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["9434"],"URL":"https:\/\/doi.org\/10.1007\/s10472-014-9434-6","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,17]]}}}