{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:30:26Z","timestamp":1767929426140,"version":"3.49.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present semantic correctness proofs of Automatic Differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Finally, we sketch how the analysis extends to other AD methods by considering a continuation-based method.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_17","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"319-338","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing"],"prefix":"10.1007","author":[{"given":"Mathieu","family":"Huot","sequence":"first","affiliation":[]},{"given":"Sam","family":"Staton","sequence":"additional","affiliation":[]},{"given":"Matthijs","family":"V\u00e1k\u00e1r","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"17_CR1","unstructured":"Abadi, M., Barham, P., Chen, J., Chen, Z., Davis, A., Dean, J., Devin, M., Ghemawat, S., Irving, G., Isard, M., et\u00a0al.: Tensorflow: A system for large-scale machine learning. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). pp. 265\u2013283 (2016)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Plotkin, G.D.: A simple differentiable programming language. In: Proc.\u00a0POPL 2020. ACM (2020)","DOI":"10.1145\/3371106"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Baez, J., Hoffnung, A.: Convenient categories of smooth spaces. Transactions of the American Mathematical Society 363(11), 5789\u20135825 (2011)","DOI":"10.1090\/S0002-9947-2011-05107-X"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crubill\u00e9, R., Lago, U.D., Gavazzo, F.: On the versatility of open logical relations: Continuity, automatic differentiation, and a containment theorem. In: Proc.\u00a0ESOP 2020. Springer (2020), to appear","DOI":"10.1007\/978-3-030-44914-8_3"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Brunel, A., Mazza, D., Pagani, M.: Backpropagation in the simply typed lambda-calculus with linear negation. In: Proc.\u00a0POPL 2020 (2020)","DOI":"10.1145\/3371132"},{"key":"17_CR6","unstructured":"Carpenter, B., Hoffman, M.D., Brubaker, M., Lee, D., Li, P., Betancourt, M.: The Stan math library: Reverse-mode automatic differentiation in C++. arXiv preprint arXiv:1509.07164 (2015)"},{"key":"17_CR7","unstructured":"Christensen, J.D., Wu, E.: Tangent spaces and tangent bundles for diffeological spaces. arXiv preprint\u00a0arXiv:1411.5425 (2014)"},{"key":"17_CR8","unstructured":"Cockett, J.R.B., Cruttwell, G.S.H., Gallagher, J., Lemay, J.S.P., MacAdam, B., Plotkin, G.D., Pronk, D.: Reverse derivative categories. In: Proc.\u00a0CSL 2020 (2020)"},{"key":"17_CR9","unstructured":"Cruttwell, G., Gallagher, J., MacAdam, B.: Towards formalizing and extending differential programming using tangent categories. In: Proc.\u00a0ACT 2019 (2019)"},{"key":"17_CR10","unstructured":"Duchi, J., Hazan, E., Singer, Y.: Adaptive subgradient methods for online learning and stochastic optimization. Journal of Machine Learning Research 12(Jul), 2121\u20132159 (2011)"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoretical Computer Science 309(1-3), 1\u201341 (2003)","DOI":"10.1016\/S0304-3975(03)00392-X"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Elliott, C.: The simple essence of automatic differentiation. Proceedings of the ACM on Programming Languages 2(ICFP), \u00a070 (2018)","DOI":"10.1145\/3236765"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Fong, B., Spivak, D., Tuy\u00e9ras, R.: Backprop as functor: A compositional perspective on supervised learning. In: 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201313. IEEE (2019)","DOI":"10.1109\/LICS.2019.8785665"},{"key":"17_CR14","unstructured":"Hoffman, M.D., Gelman, A.: The No-U-Turn sampler: adaptively setting path lengths in Hamiltonian Monte Carlo. Journal of Machine Learning Research 15(1), 1593\u20131623 (2014)"},{"key":"17_CR15","unstructured":"Huot, M., Staton, S., V\u00e1k\u00e1r, M.: Correctness of automatic differentiation via diffeologies and categorical gluing. Full version (2020),\u00a0arxiv:2001.02209"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Iglesias-Zemmour, P.: Diffeology. American Mathematical Soc. (2013)","DOI":"10.1090\/surv\/185"},{"key":"17_CR17","unstructured":"Johnstone, P.T., Lack, S., Sobocinski, P.: Quasitoposes, quasiadhesive categories and Artin glueing. In: Proc.\u00a0CALCO 2007 (2007)"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Kiefer, J., Wolfowitz, J., et\u00a0al.: Stochastic estimation of the maximum of a regression function. The Annals of Mathematical Statistics 23(3), 462\u2013466 (1952)","DOI":"10.1214\/aoms\/1177729392"},{"key":"17_CR19","unstructured":"Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. arXiv preprint\u00a0arxiv:1412.6980 (2014)"},{"key":"17_CR20","unstructured":"Kucukelbir, A., Tran, D., Ranganath, R., Gelman, A., Blei, D.M.: Automatic differentiation variational inference. The Journal of Machine Learning Research 18(1), 430\u2013474 (2017)"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Liu, D.C., Nocedal, J.: On the limited memory BFGS method for large scale optimization. Mathematical programming 45(1-3), 503\u2013528 (1989)","DOI":"10.1007\/BF01589116"},{"key":"17_CR22","unstructured":"Mak, C., Ong, L.: A differential-form pullback programming language for higher-order reverse-mode automatic differentiation (2020),\u00a0arxiv:2002.08241"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Manzyuk, O.: A simply typed $$\\lambda $$-calculus of forward automatic differentiation. In: Proc.\u00a0MFPS 2012 (2012)","DOI":"10.1016\/j.entcs.2012.08.017"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Scedrov, A.: Notes on sconing and relators. In: International Workshop on Computer Science Logic. pp. 352\u2013378. Springer (1992)","DOI":"10.1007\/3-540-56992-8_21"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Neal, R.M., et\u00a0al.: MCMC using Hamiltonian dynamics. Handbook of Markov Chain Monte Carlo 2(11), \u00a02 (2011)","DOI":"10.1201\/b10905-6"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Pearlmutter, B.A., Siskind, J.M.: Reverse-mode AD in a functional framework: Lambda the ultimate backpropagator. ACM Transactions on Programming Languages and Systems (TOPLAS) 30(2), \u00a07 (2008)","DOI":"10.1145\/1330017.1330018"},{"key":"17_CR27","unstructured":"Pitts, A.M.: Categorical logic. Tech. rep., University of Cambridge, Computer Laboratory (1995)"},{"key":"17_CR28","unstructured":"Plotkin, G.D.: Some principles of differential programming languages (2018), invited talk, POPL 2018"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Qian, N.: On the momentum term in gradient descent learning algorithms. Neural networks 12(1), 145\u2013151 (1999)","DOI":"10.1016\/S0893-6080(98)00116-6"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Robbins, H., Monro, S.: A stochastic approximation method. The annals of mathematical statistics pp. 400\u2013407 (1951)","DOI":"10.1214\/aoms\/1177729586"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Shaikhha, A., Fitzgibbon, A., Vytiniotis, D., Peyton\u00a0Jones, S.: Efficient differentiable programming in a functional array-processing language. Proceedings of the ACM on Programming Languages 3(ICFP), \u00a097 (2019)","DOI":"10.1145\/3341701"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Souriau, J.M.: Groupes diff\u00e9rentiels. In: Differential geometrical methods in mathematical physics, pp. 91\u2013128. Springer (1980)","DOI":"10.1007\/BFb0089728"},{"key":"17_CR33","unstructured":"Stacey, A.: Comparative smootheology. Theory Appl. Categ. 25(4), 64\u2013117 (2011)"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Wang, F., Wu, X., Essertel, G., Decker, J., Rompf, T.: Demystifying differentiable programming: Shift\/reset the penultimate backpropagator. Proceedings of the ACM on Programming Languages 3(ICFP) (2019)","DOI":"10.1145\/3341700"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T13:38:47Z","timestamp":1610026727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}