{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:42:34Z","timestamp":1742946154229,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_23","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"312-324","source":"Crossref","is-referenced-by-count":4,"title":["Automatic Differentiation in ACL2"],"prefix":"10.1007","author":[{"given":"Peter","family":"Reid","sequence":"first","affiliation":[]},{"given":"Ruben","family":"Gamboa","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"Community portal for automatic differentiation, http:\/\/www.autodiff.org"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Corliss, G., Griewank, A., Bischof, C., Carle, A., Hovland, P.: ADIFOR: Generating derivative codes from fortran programs. Scientific Programming\u00a0(1) (1991)","DOI":"10.1155\/1992\/717832"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Roh, L., Bischof, C., Mauer-oats, A.: ADIC: An extensible automatic differentiation tool for ANSI-C\u00a027, 1427\u20131456 (1997)","DOI":"10.1002\/(SICI)1097-024X(199712)27:12<1427::AID-SPE138>3.0.CO;2-Q"},{"key":"23_CR4","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/s10990-008-9034-4","volume":"21","author":"P.D. Hovland","year":"2008","unstructured":"Hovland, P.D., Bischof, C.H., Norris, B.: On the implementation of automatic differentiation tools. Higher Order Symbol. Comput.\u00a021, 311\u2013331 (2008)","journal-title":"Higher Order Symbol. Comput."},{"key":"23_CR5","series-title":"CIS","volume-title":"Automatic Differentiation of Algorithms: From Simulation to Optimization","year":"2001","unstructured":"Corliss, G., Faure, C., Griewank, A., Hascoet, L., Naumann, U. (eds.): Automatic Differentiation of Algorithms: From Simulation to Optimization. CIS. Springer, Heidelberg (2001); Selected papers from the AD2000 conference, Nice, France (June 2000)"},{"key":"23_CR6","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"R. Gamboa","year":"2000","unstructured":"Gamboa, R.: Continuity and differentiability in ACL2. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, ch. 18. Kluwer Academic Press, Dordrecht (2000)"},{"key":"23_CR7","unstructured":"Gamboa, R., Cowles, J.: The chain rule and friends in ACL2(r). In: Proceedings of the Eighth International Workshop of the ACL2 Theorem Prover and its Applications, ACL2 2009 (2009)"},{"issue":"4","key":"23_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1023\/A:1011908113514","volume":"27","author":"R. Gamboa","year":"2001","unstructured":"Gamboa, R., Kaufmann, M.: Nonstandard analysis in ACL2. Journal of Automated Reasoning\u00a027(4), 323\u2013351 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR9","series-title":"Other Titles in Applied Mathematics","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717761","volume-title":"Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation","author":"A. Griewank","year":"2008","unstructured":"Griewank, A., Walthe, A.: Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation. Other Titles in Applied Mathematics. SIAM, Philadelphia (2008)"},{"key":"23_CR10","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M.: Modular proof: The fundamental theorem of calculus. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, ch. 6, Kluwer Academic Press, Dordrecht (2000)"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Pearlmutter, A.B., Siskind, J.M.: Reverse-mode AD in a functional framework: Lambda the ultimate backpropagator. ACM Trans. Program. Lang. Syst.\u00a030, 7:1\u20137:36 (2008)","DOI":"10.1145\/1330017.1330018"},{"key":"23_CR12","series-title":"LNCSE","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-68942-3_3","volume-title":"Advances in Automatic Differentiation","author":"E.M. Tadjouddine","year":"2008","unstructured":"Tadjouddine, E.M.: On formal certification of AD transformations. In: Barth, T.J., et al. (eds.) MFCS 1978. LNCSE, vol.\u00a064, pp. 23\u201333. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T18:13:39Z","timestamp":1560449619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}