{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:01:58Z","timestamp":1750309318100,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"German Federal Ministry of Education and Research and the Hessian Ministry of Higher Education, Research, Science and the Arts","award":["National Research Center for Applied Cybersecurity ATHENE"],"award-info":[{"award-number":["National Research Center for Applied Cybersecurity ATHENE"]}]},{"name":"Hessian Ministry of Higher Education, Research, Science and the Arts","award":["3rd Wave of AI"],"award-info":[{"award-number":["3rd Wave of AI"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,7,18]]},"DOI":"10.1145\/3605156.3606456","type":"proceedings-article","created":{"date-parts":[[2023,7,13]],"date-time":"2023-07-13T21:02:37Z","timestamp":1689282157000},"page":"51-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Using Rewrite Strategies for Efficient Functional Automatic Differentiation"],"prefix":"10.1145","author":[{"given":"Timon","family":"B\u00f6hler","sequence":"first","affiliation":[{"name":"TU Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Richter","sequence":"additional","affiliation":[{"name":"TU Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mira","family":"Mezini","sequence":"additional","affiliation":[{"name":"TU Darmstadt, Germany \/ hessian.AI, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"622","article-title":"Cartesian differential categories","volume":"22","author":"Blute Richard F","year":"2009","unstructured":"Richard F Blute , J Robin B Cockett , and Robert AG Seely . 2009 . Cartesian differential categories . Theory and Applications of Categories , 22 , 23 (2009), 622 \u2013 672 . Richard F Blute, J Robin B Cockett, and Robert AG Seely. 2009. Cartesian differential categories. Theory and Applications of Categories, 22, 23 (2009), 622\u2013672.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_2_1_2_1","volume-title":"Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang.","author":"Bradbury James","year":"2018","unstructured":"James Bradbury , Roy Frostig , Peter Hawkins , Matthew James Johnson , Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. 2018 . JAX: composable transformations of Python +NumPy programs. http:\/\/github.com\/google\/jax James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. 2018. JAX: composable transformations of Python+NumPy programs. http:\/\/github.com\/google\/jax"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.013"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.18"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.333.20"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_1_8_1","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2021. Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. arXiv preprint arXiv:2112.07292. \t\t\t\t  Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2021. Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. arXiv preprint arXiv:2112.07292."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236765"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408974"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450153.2450158"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062354"},{"key":"e_1_3_2_1_13_1","volume-title":"Don\u2019t Unroll Adjoint: Differentiating SSA-Form Programs. CoRR, abs\/1810.07951","author":"Innes Michael","year":"2018","unstructured":"Michael Innes . 2018. Don\u2019t Unroll Adjoint: Differentiating SSA-Form Programs. CoRR, abs\/1810.07951 ( 2018 ), arXiv:1810.07951. arxiv:1810.07951 Michael Innes. 2018. Don\u2019t Unroll Adjoint: Differentiating SSA-Form Programs. CoRR, abs\/1810.07951 (2018), arXiv:1810.07951. arxiv:1810.07951"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004331"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434309"},{"key":"e_1_3_2_1_16_1","unstructured":"Samuel Mimram. 2020. PROGRAM = PROOF. \t\t\t\t  Samuel Mimram. 2020. PROGRAM = PROOF."},{"key":"e_1_3_2_1_17_1","volume-title":"Automatically Synthesize Fast Gradients. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020","author":"William","year":"2020","unstructured":"William S. Moses and Valentin Churavy. 2020. Instead of Rewriting Foreign Code for Machine Learning , Automatically Synthesize Fast Gradients. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020 , NeurIPS 2020 , December 6-12, 2020, virtual, Hugo Larochelle, Marc\u2019Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (Eds.). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/9332c513ef44b682e9347822c2e457ac-Abstract.html William S. Moses and Valentin Churavy. 2020. Instead of Rewriting Foreign Code for Machine Learning, Automatically Synthesize Fast Gradients. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, Hugo Larochelle, Marc\u2019Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (Eds.). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/9332c513ef44b682e9347822c2e457ac-Abstract.html"},{"key":"e_1_3_2_1_18_1","volume-title":"High-Performance Deep Learning Library. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019","author":"Paszke Adam","year":"2019","unstructured":"Adam Paszke , Sam Gross , Francisco Massa , Adam Lerer , James Bradbury , Gregory Chanan , Trevor Killeen , Zeming Lin , Natalia Gimelshein , Luca Antiga , Alban Desmaison , Andreas K\u00f6pf , Edward Z. Yang , Zachary DeVito , Martin Raison , Alykhan Tejani , Sasank Chilamkurthy , Benoit Steiner , Lu Fang , Junjie Bai , and Soumith Chintala . 2019 . PyTorch: An Imperative Style , High-Performance Deep Learning Library. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 , NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d\u2019Alch\u00e9-Buc, Emily B. Fox, and Roman Garnett (Eds.). 8024\u20138035. https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/bdbca288fee7f92f2bfa9f7012727740-Abstract.html Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas K\u00f6pf, Edward Z. Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. 2019. PyTorch: An Imperative Style, High-Performance Deep Learning Library. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d\u2019Alch\u00e9-Buc, Emily B. Fox, and Roman Garnett (Eds.). 8024\u20138035. https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/bdbca288fee7f92f2bfa9f7012727740-Abstract.html"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473593"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122948.3122949"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341701"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.12.011"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289425"},{"key":"e_1_3_2_1_24_1","volume-title":"Demystifying Differentiable Programming: Shift\/Reset the Penultimate Backpropagator. CoRR, abs\/1803.10228","author":"Wang Fei","year":"2018","unstructured":"Fei Wang , Xilun Wu , Gr\u00e9gory M. Essertel , James M. Decker , and Tiark Rompf . 2018. Demystifying Differentiable Programming: Shift\/Reset the Penultimate Backpropagator. CoRR, abs\/1803.10228 ( 2018 ), arXiv:1803.10228. arxiv:1803.10228 Fei Wang, Xilun Wu, Gr\u00e9gory M. Essertel, James M. Decker, and Tiark Rompf. 2018. Demystifying Differentiable Programming: Shift\/Reset the Penultimate Backpropagator. CoRR, abs\/1803.10228 (2018), arXiv:1803.10228. arxiv:1803.10228"},{"key":"e_1_3_2_1_25_1","volume-title":"Deep Learning has outlived its usefulness... | Facebook. https:\/\/web.archive.org\/web\/20180106001630\/https:\/\/www.facebook.com\/yann.lecun\/posts\/10155003011462143 [Online","author":"LeCun Yann","year":"2022","unstructured":"Yann LeCun . 2018. Yann LeCun - OK , Deep Learning has outlived its usefulness... | Facebook. https:\/\/web.archive.org\/web\/20180106001630\/https:\/\/www.facebook.com\/yann.lecun\/posts\/10155003011462143 [Online ; accessed 7- April - 2022 ] Yann LeCun. 2018. Yann LeCun - OK, Deep Learning has outlived its usefulness... | Facebook. https:\/\/web.archive.org\/web\/20180106001630\/https:\/\/www.facebook.com\/yann.lecun\/posts\/10155003011462143 [Online; accessed 7-April-2022]"}],"event":{"name":"FTfJP '23: 25th ACM International Workshop on Formal Techniques for Java-like Programs","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"],"location":"Seattle WA USA","acronym":"FTfJP '23"},"container-title":["Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605156.3606456","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:54Z","timestamp":1750291434000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3605156.3606456"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,18]]},"references-count":25,"alternative-id":["10.1145\/3605156.3606456","10.1145\/3605156"],"URL":"https:\/\/doi.org\/10.1145\/3605156.3606456","relation":{},"subject":[],"published":{"date-parts":[[2023,7,18]]},"assertion":[{"value":"2023-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}