{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:07Z","timestamp":1751660527136,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show how to define forward- and reverse-mode automatic differentiation source-code transformations or on a standard higher-order functional language. The transformations generate purely functional code, and they are principled in the sense that their definition arises from a categorical universal property. We give a semantic proof of correctness of the transformations. In their most elegant formulation, the transformations generate code with linear types. However, we demonstrate how the transformations can be implemented in a standard functional language without sacrificing correctness. To do so, we make use of abstract data types to represent the required linear types, e.g. through the use of a basic module system.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_22","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"607-634","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Reverse AD at Higher Types: Pure, Principled and Denotationally Correct"],"prefix":"10.1007","author":[{"given":"Matthijs","family":"V\u00e1k\u00e1r","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"unstructured":"Abadi, M., Barham, P., Chen, J., Chen, Z., Davis, A., Dean, J., Devin, M., Ghemawat, S., Irving, G., Isard, M., et al.: 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":"22_CR1"},{"doi-asserted-by":"crossref","unstructured":"Abadi, M., Plotkin, G.D.: A simple differentiable programming language. In: Proc. POPL 2020. ACM (2020)","key":"22_CR2","DOI":"10.1145\/3371106"},{"doi-asserted-by":"crossref","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Categories of containers. In: International Conference on Foundations of Software Science and Computation Structures. pp. 23\u201338. Springer (2003)","key":"22_CR3","DOI":"10.1007\/3-540-36576-1_2"},{"unstructured":"Barber, A., Plotkin, G.: Dual intuitionistic linear logic. University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science (1996)","key":"22_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. ESOP 2020. Springer (2020), to appear","key":"22_CR5","DOI":"10.1007\/978-3-030-44914-8_3"},{"doi-asserted-by":"crossref","unstructured":"Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models. In: International Workshop on Computer Science Logic. pp. 121\u2013135. Springer (1994)","key":"22_CR6","DOI":"10.1007\/BFb0022251"},{"unstructured":"Blute, R., Ehrhard, T., Tasson, C.: A convenient differential category. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques 53(3), 211\u2013232 (2012)","key":"22_CR7"},{"doi-asserted-by":"crossref","unstructured":"Brunel, A., Mazza, D., Pagani, M.: Backpropagation in the simply typed lambda-calculus with linear negation. In: Proc. POPL 2020 (2020)","key":"22_CR8","DOI":"10.1145\/3371132"},{"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 $${\\text{arXiv:}}$$1509.07164 (2015)","key":"22_CR9"},{"doi-asserted-by":"crossref","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Information and Computation 179(1), 19\u201375 (2002)","key":"22_CR10","DOI":"10.1006\/inco.2001.2951"},{"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. CSL 2020 (2020)","key":"22_CR11"},{"doi-asserted-by":"crossref","unstructured":"Curien, P.L.: Categorical combinators. Information and Control 69(1\u20133), 188\u2013254 (1986)","key":"22_CR12","DOI":"10.1016\/S0019-9958(86)80047-X"},{"doi-asserted-by":"crossref","unstructured":"Curien, P.L.: Typed categorical combinatory logic. In: Colloquium on Trees in Algebra and Programming. pp. 157\u2013172. Springer (1985)","key":"22_CR13","DOI":"10.1007\/3-540-15198-2_10"},{"doi-asserted-by":"crossref","unstructured":"Egger, J., M\u00f8gelberg, R.E., Simpson, A.: Enriching an effect calculus with linear types. In: International Workshop on Computer Science Logic. pp. 240\u2013254. Springer (2009)","key":"22_CR14","DOI":"10.1007\/978-3-642-04027-6_19"},{"doi-asserted-by":"crossref","unstructured":"Ehrhard, T.: An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28(7), 995\u20131060 (2018)","key":"22_CR15","DOI":"10.1017\/S0960129516000372"},{"doi-asserted-by":"crossref","unstructured":"Elliott, C.: The simple essence of automatic differentiation. Proceedings of the ACM on Programming Languages 2(ICFP), 70 (2018)","key":"22_CR16","DOI":"10.1145\/3236765"},{"doi-asserted-by":"crossref","unstructured":"Fiore, M.P.: Differential structure in models of multiplicative biadditive intuitionistic linear logic. In: International Conference on Typed Lambda Calculi and Applications. pp. 163\u2013177. Springer (2007)","key":"22_CR17","DOI":"10.1007\/978-3-540-73228-0_13"},{"doi-asserted-by":"crossref","unstructured":"Fr\u00f6licher, A.: Smooth structures. In: Category theory. pp. 69\u201381. Springer (1982)","key":"22_CR18","DOI":"10.1007\/BFb0066887"},{"unstructured":"Fr\u00f6licher, A.: Linear spaces and differentiation theory. Pure and Applied Mathematics (1988)","key":"22_CR19"},{"doi-asserted-by":"crossref","unstructured":"Huot, M., Staton, S., V\u00e1k\u00e1r, M.: Correctness of automatic differentiation via diffeologies and categorical gluing. In: Proc. FoSSaCS (2020)","key":"22_CR20","DOI":"10.1007\/978-3-030-45231-5_17"},{"doi-asserted-by":"crossref","unstructured":"Iglesias-Zemmour, P.: Diffeology. American Mathematical Soc. (2013)","key":"22_CR21","DOI":"10.1090\/surv\/185"},{"unstructured":"Innes, M.: Don\u2019t unroll adjoint: differentiating SSA-Form programs. arXiv preprint $${\\text{ arXiv: }}$$1810.07951","key":"22_CR22"},{"doi-asserted-by":"crossref","unstructured":"Johnstone, P.T.: Sketches of an elephant: A topos theory compendium, vol. 2. Oxford University Press (2002)","key":"22_CR23","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"unstructured":"Johnstone, P.T., Lack, S., Sobocinski, P.: Quasitoposes, quasiadhesive categories and Artin glueing. In: Proc. CALCO 2007 (2007)","key":"22_CR24"},{"doi-asserted-by":"crossref","unstructured":"Kock, A.: Synthetic differential geometry, vol. 333. Cambridge University Press (2006)","key":"22_CR25","DOI":"10.1017\/CBO9780511550812"},{"unstructured":"Lambek, J., Scott, P.J.: Introduction to higher-order categorical logic, vol. 7. Cambridge University Press (1988)","key":"22_CR26"},{"unstructured":"Levy, P.B.: Call-by-push-value: A Functional\/imperative Synthesis, vol. 2. Springer Science & Business Media (2012)","key":"22_CR27"},{"unstructured":"Mak, C., Ong, L.: A differential-form pullback programming language for higher-order reverse-mode automatic differentiation (2020), $${\\text{ arXiv: }}$$2002.08241","key":"22_CR28"},{"unstructured":"Mellies, P.A.: Categorical semantics of linear logic. Panoramas et syntheses 27, 15\u2013215 (2009)","key":"22_CR29"},{"unstructured":"Paszke, A., Gross, S., Chintala, S., Chanan, G., Yang, E., DeVito, Z., Lin, Z., Desmaison, A., Antiga, L., Lerer, A.: Automatic differentiation in pytorch (2017)","key":"22_CR30"},{"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), 7 (2008)","key":"22_CR31","DOI":"10.1145\/1330017.1330018"},{"doi-asserted-by":"crossref","unstructured":"Shaikhha, A., Fitzgibbon, A., Vytiniotis, D., Peyton Jones, S.: Efficient differentiable programming in a functional array-processing language. Proceedings of the ACM on Programming Languages 3(ICFP), 97 (2019)","key":"22_CR32","DOI":"10.1145\/3341701"},{"doi-asserted-by":"crossref","unstructured":"Souriau, J.M.: Groupes diff\u00e9rentiels. In: Differential geometrical methods in mathematical physics, pp. 91\u2013128. Springer (1980)","key":"22_CR33","DOI":"10.1007\/BFb0089728"},{"doi-asserted-by":"crossref","unstructured":"V\u00e1k\u00e1r, M.: A categorical semantics for linear logical frameworks. In: International Conference on Foundations of Software Science and Computation Structures. pp. 102\u2013116. Springer (2015)","key":"22_CR34","DOI":"10.1007\/978-3-662-46678-0_7"},{"unstructured":"V\u00e1k\u00e1r, M.: Denotational correctness of forward-mode automatic differentiation for iteration and recursion. arXiv preprint $${\\text{ arXiv: }}$$2007.05282 (2020)","key":"22_CR35"},{"doi-asserted-by":"crossref","unstructured":"V\u00e1k\u00e1r, M.: Reverse ad at higher types: Pure, principled and denotationally correct (full version). arXiv preprint $${\\text{ arXiv: }}$$2007.05283 (2020)","key":"22_CR36","DOI":"10.26226\/morressier.604907f41a80aac83ca25d18"},{"unstructured":"Vytiniotis, D., Belov, D., Wei, R., Plotkin, G., Abadi, M.: The differentiable curry (2019)","key":"22_CR37"},{"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)","key":"22_CR38","DOI":"10.1145\/3341700"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T15:36:01Z","timestamp":1724686561000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","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":"79","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":"24","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":"30% - 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-5","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":"10","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 took place virtually due to the COVID-19 pandemic","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)"}}]}}