{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:15:00Z","timestamp":1775873700427,"version":"3.50.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NWO","award":["VI.Veni.202.124"],"award-info":[{"award-number":["VI.Veni.202.124"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>We show how the basic Combinatory Homomorphic Automatic Differentiation (CHAD) algorithm can be optimised, using well-known methods, to yield a simple, composable, and generally applicable reverse-mode automatic differentiation (AD) technique that has the correct computational complexity that we would expect of reverse-mode AD. Specifically, we show that the standard optimisations of sparse vectors and state-passing style code (as well as defunctionalisation\/closure conversion, for higher-order languages) give us a purely functional algorithm that is most of the way to the correct complexity, with (functional) mutable updates taking care of the final log-factors. We provide an Agda formalisation of our complexity proof. Finally, we discuss how the techniques apply to differentiating parallel functional array programs: the key observations are 1) that all required mutability is (commutative, associative) accumulation, which lets us preserve task-parallelism and 2) that we can write down data-parallel derivatives for most data-parallel array primitives.<\/jats:p>","DOI":"10.1145\/3632878","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1060-1088","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Efficient CHAD"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4986-6820","authenticated-orcid":false,"given":"Tom J.","family":"Smeding","sequence":"first","affiliation":[{"name":"Utrecht University, Utrecht, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4603-0523","authenticated-orcid":false,"given":"Matthijs I. L.","family":"V\u00e1k\u00e1r","sequence":"additional","affiliation":[{"name":"Utrecht University, Utrecht, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","first-page":"265","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016","author":"Abadi Mart\u00edn","year":"2016","unstructured":"Mart\u00edn Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, Manjunath Kudlur, Josh Levenberg, Rajat Monga, Sherry Moore, Derek Gordon Murray, Benoit Steiner, Paul A. Tucker, Vijay Vasudevan, Pete Warden, Martin Wicke, Yuan Yu, Xiaoqiang Zheng. 2016. TensorFlow: A System for Large-Scale Machine Learning. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, Kimberly Keeton, Timothy Roscoe. USENIX Association, 265\u2013283. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/abadi"},{"key":"e_1_3_1_3_1","unstructured":"Accelerate contributors. 2020. Data.Array.Accelerate (accelerate-1.3.0.0). https:\/\/hackage.haskell.org\/package\/accelerate-1.3.0.0\/docs\/Data-Array-Accelerate.html. Accessed: 2020-11-28."},{"key":"e_1_3_1_4_1","unstructured":"Mario Alvarez-Picallo Dan R. Ghica David Sprunger and Fabio Zanasi. 2021. Functorial String Diagrams for Reverse-Mode Automatic Differentiation. CoRR abs\/2107.13433 (2021). arXiv:2107.13433 https:\/\/arxiv.org\/abs\/2107.13433"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_3"},{"key":"e_1_3_1_6_1","first-page":"153:1","article-title":"Automatic Differentiation in Machine Learning: a Survey","volume":"18","author":"Baydin Atilim Gunes","year":"2017","unstructured":"Atilim Gunes Baydin, Barak A. Pearlmutter, Alexey Andreyevich Radul, and Jeffrey Mark Siskind. 2017. Automatic Differentiation in Machine Learning: a Survey. J. Mach. Learn. Res. 18 (2017), 153:1\u2013153:43. http:\/\/jmlr.org\/papers\/v18\/17-468.html","journal-title":"J. Mach. Learn. Res."},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_1_8_1","unstructured":"James Bradbury Roy Frostig Peter Hawkins Matthew James Johnson Chris Leary Dougal Maclaurin George Necula Adam Paszke Jake VanderPlas Skye Wanderman-Milne Qiao Zhang. 2018. JAX: composable transformations of Python+NumPy programs. http:\/\/github.com\/google\/jax"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/322123.322127"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926354.1926358"},{"key":"e_1_3_1_11_1","unstructured":"Curtis Chin Jen Sem. 2020. Formalized Correctness Proofs of Automatic Differentiation in Coq. Master\u2019s Thesis Utrecht University (09 2020). https:\/\/dspace.library.uu.nl\/handle\/1874\/400790; Coq code: https:\/\/github.com\/crtschin\/thesis."},{"key":"e_1_3_1_12_1","unstructured":"Paulo Em\u00edlio de Vilhena Fran\u00e7ois Pottier. 2021. Verifying a Minimalist Reverse-Mode AD Library. arXiv preprint arXiv:2112.07292 (2021)."},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236765"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.360.1"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Andreas Griewank Andrea Walther. 2008. Evaluating derivatives - principles and techniques of algorithmic differentiation Second Edition. SIAM. https:\/\/doi.org\/10.1137\/1.9780898717761 10.1137\/1.9780898717761","DOI":"10.1137\/1.9780898717761"},{"key":"e_1_3_1_16_1","unstructured":"Troels Henriksen. 2017. Design and Implementation of the Futhark Programming Language. Ph.D. Dissertation. University of Copenhagen Universitetsparken 5 2100 K\u00f8benhavn."},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062354"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90059-1"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_17"},{"key":"e_1_3_1_20_1","unstructured":"Mathieu Huot Sam Staton Matthijs V\u00e1k\u00e1r. 2021. Higher Order Automatic Differentiation of Higher Order Functions. CoRR abs\/2101.06757 (2021). arXiv:2101.06757 https:\/\/arxiv.org\/abs\/2101.06757"},{"key":"e_1_3_1_21_1","unstructured":"Marie Kerjean Pierre-Marie P\u00e9drot. 2022. \ud835\udf15 is for Dialectica. (Jan. 2022). https:\/\/hal.archives-ouvertes.fr\/hal-03123968 working paper or preprint."},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498710"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676969"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178246"},{"key":"e_1_3_1_25_1","volume-title":"TensorFlow Dev Summit","author":"Leary Chris","year":"2017","unstructured":"Chris Leary, Todd Wang. 2017. XLA: TensorFlow, compiled. TensorFlow Dev Summit (2017). https:\/\/developers.googleblog.com\/2017\/03\/xla-tensorflow-compiled.html"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01931367"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1002\/widm.1305"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500595"},{"key":"e_1_3_1_29_1","volume-title":"Technical Report NVR-2016-002. NVIDIA","author":"Merrill Duane","year":"2016","unstructured":"Duane Merrill, Michael Garland. 2016. Single-pass Parallel Prefix Scan with Decoupled Look-back. Technical Report NVR-2016-002. NVIDIA."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237791"},{"key":"e_1_3_1_31_1","unstructured":"Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Vol. 32. Chalmers University of Technology."},{"key":"e_1_3_1_32_1","unstructured":"Fernando Lucatelli Nunes Matthijs V\u00e1k\u00e1r. 2022. Automatic Differentiation for ML-family languages: correctness via logical relations. CoRR abs\/2210.07724 (2022). arXiv:2210.07724 https:\/\/arxiv.org\/abs\/2210.07724"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012952300018X"},{"key":"e_1_3_1_34_1","volume-title":"NIPS 2017 Autodiff Workshop: The future of gradient-based machine learning software and techniques","author":"Paszke Adam","year":"2017","unstructured":"Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, Adam Lerer. 2017. Automatic differentiation in PyTorch. In NIPS 2017 Autodiff Workshop: The future of gradient-based machine learning software and techniques. Curran Associates, Inc., Red Hook, NY, USA."},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473593"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3471873.3472975"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1330017.1330018"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571236"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_3_1_42_1","unstructured":"Robert Schenck Ola R\u00f8nning Troels Henriksen Cosmin E. Oancea. 2022. AD for an Array Language with Nested Parallelism. CoRR abs\/2202.10297 (2022). arXiv:2202.10297 https:\/\/arxiv.org\/abs\/2202.10297"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341701"},{"key":"e_1_3_1_44_1","unstructured":"Amir Shaikhha Mathieu Huot Shideh Hashemian. 2023. \u2207SD: Differentiable Programming for Sparse Tensors. arXiv preprint arXiv:2303.07030 (2023)."},{"key":"e_1_3_1_45_1","unstructured":"Jeffrey Mark Siskind Barak A. Pearlmutter. 2016. Efficient Implementation of a Higher-Order Language with Built-In AD. CoRR abs\/1611.03416 (2016). arXiv:1611.03416"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","unstructured":"Tom Smeding Matthijs V\u00e1k\u00e1r. 2023a. Artifact for Efficient CHAD. https:\/\/doi.org\/10.5281\/zenodo.10015321 10.5281\/zenodo.10015321 Artifact for this publication.","DOI":"10.5281\/zenodo.10015321"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","unstructured":"Tom Smeding Matthijs V\u00e1k\u00e1r. 2023b. Efficient CHAD. CoRR abs\/2307.05738 (2023). https:\/\/doi.org\/10.48550\/arXiv.2307.05738 10.48550\/arXiv.2307.05738 arXiv:2307.05738","DOI":"10.48550\/arXiv.2307.05738"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571247"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_5"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_22"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527634"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2023.103010"},{"key":"e_1_3_1_53_1","unstructured":"Dimitrios Vytiniotis Dan Belov Richard Wei Gordon Plotkin Martin Abadi. 2019. The differentiable curry. NeurIPS Workshop on Program Transformations (2019)."},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_7"},{"key":"e_1_3_1_55_1","unstructured":"Matthijs V\u00e1k\u00e1r. 2020. Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion. CoRR abs\/2007.05282 (2020). arXiv:2007.05282 https:\/\/arxiv.org\/abs\/2007.05282"},{"key":"e_1_3_1_56_1","first-page":"10201","volume-title":"Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montr\u00e9al, Canada","author":"Wang Fei","year":"2018","unstructured":"Fei Wang, James M. Decker, Xilun Wu, Gr\u00e9gory M. Essertel, Tiark Rompf. 2018. Backpropagation with Callbacks: Foundations for Efficient and Expressive Differentiable Programming. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montr\u00e9al, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, Roman Garnett. 10201\u201310212. http:\/\/papers.nips.cc\/paper\/8221-backpropagation-with-callbacks-foundations-for-efficient-andexpressive-differentiable-programming"},{"key":"e_1_3_1_57_1","volume-title":"6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Workshop Track Proceedings","author":"Wang Fei","year":"2018","unstructured":"Fei Wang, Tiark Rompf. 2018. A Language and Compiler View on Differentiable Programming. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Workshop Track Proceedings. OpenReview.net. https:\/\/openreview.net\/forum?id=SJxJtYkPG"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341700"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632878","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632878","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:08Z","timestamp":1751659628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632878"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":57,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632878"],"URL":"https:\/\/doi.org\/10.1145\/3632878","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}