{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:28:07Z","timestamp":1755217687470,"version":"3.43.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>In this paper we demonstrate a technique for developing high performance applications  \nwith strong correctness guarantees. Using a theorem prover, we derive a high-level  \nspecification of the application that includes correctness invariants of our choice.  \nAfter that, within the same theorem prover, we implement an extraction of the  \nspecified application into a high-performance language of our choice. Concretely,  \nwe are using Agda to specify a framework for automatic differentiation (reverse mode)  \nthat is focused on index-safe tensors. This framework comes  \nwith an optimiser for tensor expressions and the ability to translate these  \nexpressions into Futhark. We specify a canonical convolutional neural network  \nwithin the proposed framework, compute the derivatives needed for the training  \nphase and then demonstrate that the generated code approaches the performance of TensorFlow  \ncode when running on a GPU.<\/jats:p>","DOI":"10.1145\/3747524","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"567-596","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Correctness Meets Performance: From Agda to Futhark"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3292-2985","authenticated-orcid":false,"given":"Artjoms","family":"\u0160inkarovs","sequence":"first","affiliation":[{"name":"University of Southampton, Southampton, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1195-9722","authenticated-orcid":false,"given":"Troels","family":"Henriksen","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Copenhagen, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Tensorflow: A system for large-scale machine learning. In 12th $USENIX$ Symposium on Operating Systems Design and Implementation ($OSDI$ 16). 265\u2013283.","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, and Michael Isard. 2016. Tensorflow: A system for large-scale machine learning. In 12th $USENIX$ Symposium on Operating Systems Design and Implementation ($OSDI$ 16). 265\u2013283."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures and Joint European Conference on Theory and Practice of Software (FOSSACS\u201903\/ETAPS\u201903)","author":"Abbott Michael","year":"2003","unstructured":"Michael Abbott, Thorsten Altenkirch, and Neil Ghani. 2003. Categories of containers. In Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures and Joint European Conference on Theory and Practice of Software (FOSSACS\u201903\/ETAPS\u201903). 23\u201338. isbn:3540008977"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.33"},{"key":"e_1_2_1_6_1","unstructured":"Agda Development Team. 2024. Agda 2.6.3 documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.3\/ Accessed [2024\/02\/28]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018613"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681500009X"},{"volume-title":"Categorical reconstruction of a reduction free normalization proof","author":"Altenkirch Thorsten","key":"e_1_2_1_10_1","unstructured":"Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science, David Pitt, David E. Rydeheard, and Peter Johnstone (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 182\u2013199. isbn:978-3-540-44661-3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737066"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3609024.3609412"},{"key":"e_1_2_1_14_1","article-title":"Automatic differentiation in machine learning: a survey","volume":"18","author":"Baydin At\u0131l\u0131m G\u00fcnes","year":"2017","unstructured":"At\u0131l\u0131m G\u00fcnes Baydin, Barak A. Pearlmutter, Alexey Andreyevich Radul, and Jeffrey Mark Siskind. 2017. Automatic differentiation in machine learning: a survey. J. Mach. Learn. Res., 18, 1 (2017), jan, 5595\u20135637. issn:1532-4435","journal-title":"J. Mach. Learn. Res."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371132"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926354.1926358"},{"key":"e_1_2_1_17_1","unstructured":"Tianqi Chen Mu Li Yutian Li Min Lin Naiyan Wang Minjie Wang Tianjun Xiao Bing Xu Chiyuan Zhang and Zheng Zhang. 2015. MXNet: A Flexible and Efficient Machine Learning Library for Heterogeneous Distributed Systems. arxiv:1512.01274."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527328"},{"volume-title":"Categorical Foundations of Gradient-Based Learning","author":"Cruttwell Geoffrey S. H.","key":"e_1_2_1_19_1","unstructured":"Geoffrey S. H. Cruttwell, Bruno Gavranovi\u0107, Neil Ghani, Paul Wilson, and Fabio Zanasi. 2022. Categorical Foundations of Gradient-Based Learning. In Programming Languages and Systems, Ilya Sergey (Ed.). Springer International Publishing, Cham. 1\u201328. isbn:978-3-030-99336-8"},{"key":"e_1_2_1_20_1","volume-title":"Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. Logical Methods in Computer Science, 19","author":"de Vilhena Paulo Em\u00edlio","year":"2023","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2023. Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library. Logical Methods in Computer Science, 19 (2023)."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.2211477"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236765"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919)","author":"Fong Brendan","year":"2021","unstructured":"Brendan Fong, David Spivak, and R\u00e9my Tuy\u00e9ras. 2021. Backprop as functor: a compositional perspective on supervised learning. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919). IEEE Press, Article 11, 13 pages."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976023"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005538"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/367766.368195"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863582"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591268"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498710"},{"key":"e_1_2_1_30_1","volume-title":"Automatic Functional Differentiation in JAX. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=gzT61ziSCu","author":"Lin Min","year":"2024","unstructured":"Min Lin. 2024. Automatic Functional Differentiation in JAX. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=gzT61ziSCu"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498717"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"volume-title":"Analytical Differentiation on a Digital Computer. Master\u2019s thesis","author":"Nolan J. F.","key":"e_1_2_1_33_1","unstructured":"J. F. Nolan. 1953. Analytical Differentiation on a Digital Computer. Master\u2019s thesis. Massachusetts Institute of Technology."},{"volume-title":"PyTorch: an imperative style, high-performance deep learning library","author":"Paszke Adam","key":"e_1_2_1_34_1","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 Yang, Zach 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. Curran Associates Inc., Red Hook, NY, USA."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473593"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the ACM on Programming Languages, 7, POPL","author":"Radul Alexey","year":"2023","unstructured":"Alexey Radul, Adam Paszke, Roy Frostig, Matthew J Johnson, and Dougal Maclaurin. 2023. You only linearize once: Tangents transpose to gradients. Proceedings of the ACM on Programming Languages, 7, POPL (2023), 1246\u20131274."},{"key":"e_1_2_1_37_1","volume-title":"Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions","author":"Sch\u00e4fer Steven","year":"2015","unstructured":"Steven Sch\u00e4fer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving, Christian Urban and Xingyuan Zhang (Eds.). Springer International Publishing, Cham. 359\u2013374. isbn:978-3-319-22102-1"},{"volume-title":"Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (SC \u201922)","author":"Schenck Robert","key":"e_1_2_1_38_1","unstructured":"Robert Schenck, Ola R\u00f8nning, Troels Henriksen, and Cosmin E. Oancea. 2022. AD for an array language with nested parallelism. In Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (SC \u201922). IEEE Press, Article 58, 15 pages. isbn:9784665454445"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004458"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_3"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632878"},{"key":"e_1_2_1_42_1","volume-title":"Implementation and Application of Functional Languages: 24th International Symposium, IFL 2012","author":"Thiemann Peter","year":"2013","unstructured":"Peter Thiemann and Manuel MT Chakravarty. 2013. Agda meets Accelerate. In Implementation and Application of Functional Languages: 24th International Symposium, IFL 2012, Oxford, UK, August 30-September 1, 2012, Revised Selected Papers 24. 174\u2013189."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2023.103010"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3609024.3609410"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460944.3464312"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3501"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747524","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:57:36Z","timestamp":1754413056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747524"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":47,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747524"],"URL":"https:\/\/doi.org\/10.1145\/3747524","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}