{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:49:39Z","timestamp":1725493779183},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540140313"},{"type":"electronic","value":"9783540391852"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-39185-1_7","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T16:13:43Z","timestamp":1193415223000},"page":"108-126","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["A Constructive Formalization of the Fundamental Theorem of Calculus"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"7_CR1","unstructured":"http:\/\/www.mizar.org"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Beeson, M., Foundations of constructive mathematics, Springer-Verlag, 1985","DOI":"10.1007\/978-3-642-68952-9"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Benthem Jutting, L. S. van, Checking Landau\u2019s \u201cGrundlagen\u201d in the Automath System, in Nederpelt, R. P., Geuvers, J. H. and de Vrijer, R. C. (Eds.), Selected Papers on Automath, North-Holland, 1994","DOI":"10.1016\/S0049-237X(08)70222-2"},{"key":"7_CR4","unstructured":"Bishop, E., Foundations of Constructive Analysis, McGraw-Hill Book Company, 1967"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Bishop, E. and Bridges, D., Constructive Analysis, Springer-Verlag, 1985","DOI":"10.1007\/978-3-642-61667-9"},{"key":"7_CR6","unstructured":"The Coq Development Team, The Coq Proof Assistant Reference Manual Version 7.2, INRIA-Rocquencourt, December 2001"},{"key":"7_CR7","unstructured":"Cruz-Filipe, L., Formalizing Real Calculus in Coq, in Theorem Proving in Higher Order Logics, Carre\u00f1o, V., Mu\u00f1oz, C. and Tahar, S. (eds.), NASA Conference Proceedings, Hampton, VA, 2002"},{"key":"7_CR8","volume-title":"Foundations of Modern Analysis","author":"J. Dieudonn\u00e9","year":"1969","unstructured":"Dieudonn\u00e9, J., Foundations of Modern Analysis, Academic Press, New York, 1969"},{"key":"7_CR9","volume-title":"Calcul Infinit\u00e9simal","author":"J. Dieudonn\u00e9","year":"1968","unstructured":"Dieudonn\u00e9, J., Calcul Infinit\u00e9simal, Hermann, Paris, 1968"},{"key":"7_CR10","series-title":"Lect Notes Comput Sci","volume-title":"9th International Conference, TPHOLs 1996","author":"B. Dutertre","year":"1996","unstructured":"Dutertre, B., Elements of Mathematical Analysis in PVS, 9th International Conference, TPHOLs 1996, Springer LNCS 1125, 1996"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Edalat, A. and Potts, P. J., A New representation for Exact real Numbers, in Electronic Notes in Theoretical Computer Science vol. 6, 1997","DOI":"10.1016\/S1571-0661(05)80166-5"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Edalat, A. and Krznaric, M., Numerical integration with Exact Arithmetic, in Proceedings of ICALP\u201999, 1999","DOI":"10.1007\/3-540-48523-6_7"},{"key":"7_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TYPES 2000 Workshop, Durham, UK","author":"H. Geuvers","year":"2000","unstructured":"Geuvers, H. and Niqui, M., Constructive Reals in Coq: Axioms and Categoricity, in Callaghan, P., Luo, Z., McKinna, J. and Pollack, R. (Eds.), Proceedings of TYPES 2000 Workshop, Durham, UK, LNCS 2277"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F. and Zwanenburg, J., The Algebraic Hierarchy of the FTA Project, in Linton, S. and Sebasitani (eds.), Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, pp. 271\u2013286, Elsevier, 2002","DOI":"10.1006\/jsco.2002.0552"},{"key":"7_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-44659-1_11","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Geuvers","year":"2000","unstructured":"Geuvers, H., Wiedijk, F. and Zwanenburg, J., Equational Reasoning via Partial Reflection, in Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Springer LNCS 1869, 162\u2013178, 2000"},{"key":"7_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-44659-1_13","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Gottliebsen","year":"2000","unstructured":"Gottliebsen, H., Transcendental Functions and Continuity Checking in PVS, in Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Springer LNCS 1869, 197\u2013214, 2000"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Harrison, J., Theorem Proving with the Real Numbers, Springer-Verlag, 1998","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"7_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1999","unstructured":"Harrison, J., A machine-checked theory of floating point arithmetic, in Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs 1999, Springer LNCS 1690, 113\u2013130, 1999"},{"key":"7_CR19","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"A. Heyting","year":"1956","unstructured":"Heyting, A., Intuitionism: an Introduction, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Company, Amsterdam, 1956"},{"key":"7_CR20","unstructured":"Mayero, M., Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique, PhD thesis, Universit\u00e9 Paris VI, d\u00e9cembre 2001"},{"key":"7_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-45685-6_17","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Mayero","year":"2002","unstructured":"Mayero, M. Using Theorem Proving for Numerical Analysis, in Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Springer LNCS 2410, 246\u2013262, 2002"},{"key":"7_CR22","unstructured":"Oostdijk, M., Generation and Presentation of Formal Mathematical Documents, Ph.D. Thesis, Technische Universiteit Eindhoven, 2001"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-39185-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T10:39:25Z","timestamp":1558262365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-39185-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540140313","9783540391852"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-39185-1_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}