{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:40Z","timestamp":1725484300740},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_17","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"246-262","source":"Crossref","is-referenced-by-count":6,"title":["Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm"],"prefix":"10.1007","author":[{"given":"Micaela","family":"Mayero","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"17_CR1","unstructured":"The ADIC Home Page, \n                    http:\/\/www-fp.mcs.anl.gov\/adic\/\n                    \n                  ."},{"key":"17_CR2","unstructured":"The PADRE2 Home Page. \n                    http:\/\/warbler.ise.chuo-u.ac.jp\/Padre2\/\n                    \n                  ."},{"key":"17_CR3","unstructured":"C. Bischof, A. Carle, P. Khademi, A. Mauer, and P. Hovland. ADIFOR2.0 user\u2019s guide. Technical Report ANL\/MCS-TM-192, CRPC-TR95516-S, Argonne National Laboratory Technical Memorandum, June 1998."},{"key":"17_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-48959-2_10","volume-title":"Proc. of TYPES\u201999","author":"P. Giannantonio Di","year":"1999","unstructured":"Pietro Di Giannantonio and Alberto Ciaffaglione. A co-inductive approach to real numbers. In Proc. of TYPES\u201999, volume 1956, pages 114\u2013130. Springer-Verlag LNCS, 1999."},{"key":"17_CR5","volume-title":"Technical Report 0224","author":"C. Faure","year":"1998","unstructured":"Christ\u00e8le Faure and Yves Papegay. Odyss\u00e9e user\u2019s guide version 1.7. Technical Report 0224, INRIA Sophia-Antipolis, September 1998."},{"key":"17_CR6","unstructured":"Jean-Christophe Filli\u00e2tre. Preuves de programmes imp\u00e9ratifs en th\u00e9ories des types. PhD thesis, Universit\u00e9 Paris-Sud, Juillet 1999."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Herman Geuvers, Freek Wiedijk, and Jan Zwanenburg. Equational Reasoning via Partial Reflection. In Proceedings of TPHOL. Springer-Verlag, August 2000.","DOI":"10.1007\/3-540-44659-1_11"},{"key":"17_CR8","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"17_CR9","unstructured":"Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. MIT Press, 1992."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"John Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"17_CR11","unstructured":"Micaela Mayero. Formalisation et automatisation de preuves en analyses \u00e9elle et num\u00e9rique. PhD thesis, Universit\u00e9 Paris 6, D\u00e9cembre 2001. \n                    \n                      http:\/\/logical.inria.fr\/~mayero\/\n                    \n                    \n                  ."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Sam Owre, Natarajan Shankar, and John Rushby. PVS: A prototype verification System. In Proceedings of CADE 11, Saratoga Springs, New York, June 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"17_CR13","unstructured":"LogiCal Project The Coq Development Team. The Coq Proof Assistant Reference Manual Version 7.2. INRIA-Rocquencourt, December 2001. \n                    \n                      http:\/\/coq.inria.fr\/doc-eng.html\n                    \n                    \n                  ."},{"key":"17_CR14","series-title":"PhD thesis","volume-title":"Control and data dependence for program transformations","author":"R. Towle","year":"1976","unstructured":"R. Towle. Control and data dependence for program transformations. PhD thesis, Univ. of Illinois, Urbana, March 1976."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T15:31:09Z","timestamp":1550331069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}