{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:43:27Z","timestamp":1770291807278,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540432876","type":"print"},{"value":"9783540458425","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_6","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T20:00:38Z","timestamp":1180209638000},"page":"79-95","source":"Crossref","is-referenced-by-count":16,"title":["Constructive Reals in Coq: Axioms and Categoricity"],"prefix":"10.1007","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[]},{"given":"Milad","family":"Niqui","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"6_CR1","volume-title":"Grundlehren der mathematischen Wissenschaften","author":"E. Bishop","year":"1985","unstructured":"E. Bishop and D. Bridges. Constructive Analysis. Number 279 in Grundlehren der mathematischen Wissenschaften. Springer, Berlin, 1985."},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0304-3975(98)00285-0","volume":"219","author":"D. Bridges","year":"1999","unstructured":"D. Bridges. Constructive mathematics: a foundation for computable analysis. Theoretical Computer Science, 219:95\u2013109, 1999.","journal-title":"Theoretical Computer Science"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"D. Bridges and S. Reeves. Constructive mathematics in theory and programming practice. Philosophia Mathematica, 7, 1999.","DOI":"10.1093\/philmat\/7.1.65"},{"key":"6_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0021090","volume-title":"Constructivity in Computer Science","author":"J. Chirimar","year":"1992","unstructured":"J. Chirimar and D. Howe. Implementing constructive real analysis. In J.P. Myers and M.J. O\u2019Donnel, editors, Constructivity in Computer Science, number 613 in LNCS, pages 165\u2013178, 1992."},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","first-page":"114","volume-title":"A coinductive approach to real numbers","author":"A. Ciaffaglione","year":"1999","unstructured":"A. Ciaffaglione and P. Di Gianantonio. A coinductive approach to real numbers. In Th. Coquand, P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Types 1999 Workshop, L\u00f6keberg, Sweden, number 1956 in LNCS, pages 114\u2013130, 2000."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"A. Ciaffaglione and P. Di Gianantonio. A tour with constructive real numbers. In Types 2000 Workshop, Durham, UK, 2001. This Volume.","DOI":"10.1007\/3-540-45842-5_3"},{"key":"6_CR7","unstructured":"D. Delahaye and M. Mayero. Field: une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en Coq. In Proceedings of JFLA 2001. INRIA, 2001."},{"key":"6_CR8","unstructured":"B. Barras et al. The Coq Proof Assistant Reference Manual, Version 7.1. INRIA, http:\/\/coq.inria.fr\/doc\/main.html , sep 2001."},{"key":"6_CR9","unstructured":"H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg. The algebraic hierarchy of the FTA project. In Calculemus 2001 Proc., pages 13\u201327, Siena, Italy, 2001."},{"key":"6_CR10","unstructured":"H. Geuvers, F. Wiedijk, J. Zwanenburg, R. Pollack, M. Niqui, and H. Barendregt. FTA project. http:\/\/www.cs.kun.nl\/gi\/projects\/fta\/ , nov 2000."},{"key":"6_CR11","volume-title":"Distinguished dissertations","author":"J. Harrison","year":"1998","unstructured":"J. Harrison. Theorem Proving with the Real Numbers. Distinguished dissertations. Springer, London, 1998."},{"key":"6_CR12","unstructured":"C. Jones. Completing the rationals and metric spaces in LEGO. In G. Huet and G. Plotkin, editors, Logical Environments, pages 297\u2013316. CUP, 1993."},{"key":"6_CR13","unstructured":"A. Troelstra and D. van Dalen. Constructivism in Mathematics, vol I, volume 121 of Studies in Logic and The Foundation of Math. North Holland, 1988. 342 pp."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:03:05Z","timestamp":1556434985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}