{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:55Z","timestamp":1780994695403,"version":"3.54.1"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations. Optimizations should understand the primitive operations of the specific application domain and thus happen on that level.<\/jats:p>\n                  <jats:p>Domain-specific languages (DSLs) fulfill these requirements. However, DSL compilers reinvent the wheel over and over again as standard optimizations, code generators, and general infrastructure &amp; boilerplate code must be reimplemented for each DSL compiler.<\/jats:p>\n                  <jats:p>\n                    This paper presents MImIR, an extensible, higher-order intermediate representation. At its core, MImIR is a pure type system and, hence, a form of a typed lambda calculus. Developers can declare the signatures of new (domain-specific) operations, called\n                    <jats:italic toggle=\"yes\">axioms<\/jats:italic>\n                    . An axiom can be the declaration of a function, a type constructor, or any other entity with a possibly polymorphic, polytypic, and\/or dependent type. This way, developers can extend MImIR at any low or high level and bundle them in a\n                    <jats:italic toggle=\"yes\">plugin<\/jats:italic>\n                    . Plugins extend the compiler and take care of optimizing and lowering the plugins' axioms.\n                  <\/jats:p>\n                  <jats:p>We show the expressiveness and effectiveness of MImIR in three case studies: Low-level plugins that operate at the same level of abstraction as LLVM, a regular-expression matching plugin, and plugins for linear algebra and automatic differentiation. We show that in all three studies, MImIR produces code that has state-of-the-art performance.<\/jats:p>","DOI":"10.1145\/3704840","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"95-125","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2444-6782","authenticated-orcid":false,"given":"Roland","family":"Lei\u00dfa","sequence":"first","affiliation":[{"name":"University of Mannheim, Mannheim, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0127-9623","authenticated-orcid":false,"given":"Marcel","family":"Ullrich","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2656-9863","authenticated-orcid":false,"given":"Joachim","family":"Meyer","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3387-2134","authenticated-orcid":false,"given":"Sebastian","family":"Hack","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","unstructured":"Nada Amin Samuel Gr\u00fctter Martin Odersky Tiark Rompf and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science Vol. 9600) Sam Lindley Conor McBride Philip W. Trinder and Donald Sannella (Eds.). Springer 249\u2013272. https:\/\/doi.org\/10.1007\/978-3-319-30936-1_14 10.1007\/978-3-319-30936-1_14","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_3_2_3_2","volume-title":"The Static Single Information Form","author":"Ananian C. Scott","year":"1999","unstructured":"C. Scott Ananian. 1999. The Static Single Information Form. Ph. D. Dissertation. Princeton University."},{"key":"e_1_3_2_4_2","unstructured":"Jason Ansel. 2022. TorchDynamo. https:\/\/github.com\/PyTorch\/TorchDynamo"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/129099"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/278283.278285"},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","unstructured":"Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2018 Oxford UK July 09-12 2018 Anuj Dawar and Erich Gr\u00e4del (Eds.). ACM 56\u201365. https:\/\/doi.org\/10.1145\/3209108.3209189 10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Siddharth Bhat and Tobias Grosser. 2022. Lambda the Ultimate SSA: Optimizing Functional Programs in SSA. In IEEE\/ACM International Symposium on Code Generation and Optimization CGO 2022 Seoul Korea Republic of April 2-6 2022 Jae W. Lee Sebastian Hack and Tatiana Shpeisman (Eds.). IEEE 1\u201311. https:\/\/doi.org\/10.1109\/CGO53902.2022.9741279 10.1109\/CGO53902.2022.9741279","DOI":"10.1109\/CGO53902.2022.9741279"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/567806.567807"},{"key":"e_1_3_2_12_2","first-page":"797","article-title":"Typed closure conversion for the calculus of constructions","author":"Bowman William J.","year":"2018","unstructured":"William J. Bowman and Amal Ahmed. 2018. Typed closure conversion for the calculus of constructions. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia,PA, USA, June 18-22, 2018. 797\u2013811. https:\/\/doi.org\/10.1145\/3192366.3192372 10.1145\/3192366.3192372","journal-title":"Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia,PA, USA, June 18-22, 2018"},{"key":"e_1_3_2_13_2","first-page":"9:1","volume-title":"35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference) (LIPIcs, Vol. 194)","author":"Brady Edwin C.","year":"2021","unstructured":"Edwin C. Brady. 2021. Idris 2: Quantitative Type Theory in Practice. In 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference) (LIPIcs, Vol. 194), Anders M\u00f8ller and Manu Sridharan (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 9:1\u20139:26. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2021.9 10.4230\/LIPICS.ECOOP.2021.9"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202534"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341643"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","unstructured":"Charles Consel. 1988. New Insights into Partial Evaluation: the SCHISM Experiment. In ESOP \u201888 2nd European Symposium on Programming Nancy France March 21-24 1988 Proceedings (Lecture Notes in Computer Science Vol. 300) Harald Ganzinger (Ed.). Springer 236\u2013246. https:\/\/doi.org\/10.1007\/3-540-19027-9_16 10.1007\/3-540-19027-9_16","DOI":"10.1007\/3-540-19027-9_16"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.2211477"},{"key":"e_1_3_2_19_2","first-page":"1","article-title":"An intermediate representation for speculative optimizations in a dynamic compiler","author":"Duboscq Gilles","year":"2013","unstructured":"Gilles Duboscq, Thomas W\u00fcrthinger, Lukas Stadler, Christian Wimmer, Doug Simon, and Hanspeter M\u00f6ssenb\u00f6ck. 2013. An intermediate representation for speculative optimizations in a dynamic compiler. In VMIL@SPLASH \u201813: Proceedings of the 7th ACM workshop on Virtual machines and intermediate languages, Indianapolis, IN, USA, 28 October 2013, Christoph Bockisch, Michael Haupt, Steve Blackburn, Hridesh Rajan, and Joseph Gil (Eds.). ACM, 1\u201310. https:\/\/doi.org\/10.1145\/2542142.2542143 10.1145\/2542142.2542143","journal-title":"VMIL@SPLASH \u201813: Proceedings of the 7th ACM workshop on Virtual machines and intermediate languages, Indianapolis, IN, USA, 28 October 2013"},{"key":"e_1_3_2_20_2","unstructured":"Hana Dus\u00edkov\u00e1. 2023. Compile Time Regular Expression in C++. https:\/\/github.com\/hanickadot\/compile-time-regular-expressions."},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan Amr Sabry Bruce F. Duba and Matthias Felleisen. 1993. The Essence of Compiling with Con- tinuations. In Proceedings of the ACM SIGPLAN\u201993 Conference on Programming Language Design and Implemen- tation (PLDI) Albuquerque New Mexico USA June 23-25 1993 Robert Cartwright (Ed.). ACM 237\u2013247. https:\/\/doi.org\/10.1145\/155090.155113 10.1145\/155090.155113","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_2_22_2","unstructured":"Free Software Foundation. 2023. std::RegEx from libstdc++ version 13.1.1. https:\/\/gcc.gnu.org\/onlinedocs\/gcc-13.1.0\/libstdc++\/api\/a07327.html."},{"key":"e_1_3_2_23_2","unstructured":"Syoyo Fujita. 2014. aobench. https:\/\/code.google.com\/archive\/p\/aobench\/."},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. 1971. Une Extension De \u013dInterpretation De G\u00f6del a \u013dAnalyse Et Son Application a \u013dElimination Des Coupures Dans \u013dAnalyse Et La Theorie Des Types. In Proceedings of the Second Scandinavian Logic Symposium J.E. Fenstad (Ed.). Studies in Logic and the Foundations of Mathematics Vol. 63. Elsevier 63\u201392. https:\/\/doi.org\/10.1016\/S0049-237X(08)70843-7 10.1016\/S0049-237X(08)70843-7","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"e_1_3_2_25_2","unstructured":"Google Brain. 2023. XLA: Optimizing Compiler for Machine Learning. https:\/\/www.tensorflow.org\/xla."},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"Paul Havlak. 1993. Construction of Thinned Gated Single-Assignment Form. In Languages and Compilers for Parallel Computing 6th International Workshop Portland Oregon USA August 12-14 1993 Proceedings (Lecture Notes in Computer Science Vol. 768) Utpal Banerjee David Gelernter Alexandru Nicolau and David A. Padua (Eds.). Springer 477\u2013499. https:\/\/doi.org\/10.1007\/3-540-57659-2_28 10.1007\/3-540-57659-2_28","DOI":"10.1007\/3-540-57659-2_28"},{"key":"e_1_3_2_27_2","unstructured":"Philip Hazel. 2021. Perl-compatible Regular Expressions v2. http:\/\/www.pcre.org\/current\/doc\/html\/pcre2.html."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","unstructured":"Richard Kelsey. 1995. A Correspondence between Continuation Passing Style and Static Single Assignment Form. In Proceedings ACM SIGPLAN Workshop on Intermediate Representations (IR\u201995) San Francisco CA USA January 22 1995 Michael D. Ernst (Ed.). ACM 13\u201323. https:\/\/doi.org\/10.1145\/202529.202532 10.1145\/202529.202532","DOI":"10.1145\/202529.202532"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Andrew Kennedy. 2007. Compiling with continuations continued. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming ICFP 2007 Freiburg Germany October 1-3 2007 Ralf Hinze and Norman Ramsey (Eds.). ACM 177\u2013190. https:\/\/doi.org\/10.1145\/1291151.1291179 10.1145\/1291151.1291179","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_3_2_31_2","article-title":"Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations in Languages with Bindings","author":"Koehler Thomas","year":"2021","unstructured":"Thomas Koehler, Phil Trinder, and Michel Steuwer. 2021. Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations in Languages with Bindings. CoRR abs\/2111.13040 (2021). arXiv:2111.13040 https:\/\/arxiv.org\/abs\/2111.13040","journal-title":"CoRR"},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","unstructured":"David A. Kranz Richard Kelsey Jonathan Rees Paul Hudak and James Philbin. 1986. ORBIT: an optimizing compiler for scheme. In Proceedings of the 1986 SIGPLAN Symposium on Compiler Construction Palo Alto California USA June 25-27 1986 Richard L. Wexelblat (Ed.). ACM 219\u2013233. https:\/\/doi.org\/10.1145\/12276.13333 10.1145\/12276.13333","DOI":"10.1145\/12276.13333"},{"key":"e_1_3_2_33_2","first-page":"75","article-title":"LLVM: A Compilation Framework for Lifelong Program Analysis & Transfor- mation","year":"2004","unstructured":"Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transfor- mation. In 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA. IEEE Computer Society, 75\u201388. https:\/\/doi.org\/10.1109\/CGO.2004.1281665 10.1109\/CGO.2004.1281665","journal-title":"2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","unstructured":"Chris Lattner Mehdi Amini Uday Bondhugula Albert Cohen Andy Davis Jacques A. Pienaar River Riddle Tatiana Shpeisman Nicolas Vasilache and Oleksandr Zinenko. 2021. MLIR: Scaling Compiler Infrastructure for Domain Specific Computation. In IEEE\/ACM International Symposium on Code Generation and Optimization CGO 2021 Seoul South Korea February 27 - March 3 2021 Jae W. Lee Mary Lou Soffa and Ayal Zaks (Eds.). IEEE 2\u201314. https:\/\/doi.org\/10.1109\/CGO51591.2021.9370308 10.1109\/CGO51591.2021.9370308","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276489"},{"key":"e_1_3_2_36_2","first-page":"202","article-title":"A graph-based higher-order intermediate representation","author":"Lei\u00dfa Roland","year":"2015","unstructured":"Roland Lei\u00dfa, Marcel K\u00f6ster and Sebastian Hack. 2015. A graph-based higher-order intermediate representation. In Proceedings of the 13th Annual IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2015,San Francisco, CA, USA, February 07 - 11, 2015. 202\u2013212. https:\/\/doi.org\/10.1109\/CGO.2015.7054200 10.1109\/CGO.2015.7054200","journal-title":"Proceedings of the 13th Annual IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2015,San Francisco, CA, USA, February 07 - 11, 2015"},{"key":"e_1_3_2_37_2","unstructured":"Roland Lei\u00dfa Marcel Ullrich Joachim Meyer and Sebastian Hack. 2024. MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age. https:\/\/doi.org\/10.5281\/zenodo.13952579 10.5281\/zenodo.13952579"},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","unstructured":"Luke Maurer Paul Downen Zena M. Ariola and Simon L. Peyton Jones. 2017. Compiling without continuations. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2017 Barcelona Spain June 18-23 2017 Albert Cohen and Martin T. Vechev (Eds.). ACM 482\u2013494. https:\/\/doi.org\/10.1145\/3062341.3062380 10.1145\/3062341.3062380","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","unstructured":"Krzysztof Maziarz Tom Ellis Alan Lawrence Andrew W. Fitzgibbon and Simon Peyton Jones. 2021. Hashing modulo alpha-equivalence. In PLDI \u201821: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation Virtual Event Canada June 20-25 2021 Stephen N. Freund and Eran Yahav (Eds.). ACM 960\u2013973. https:\/\/doi.org\/10.1145\/3453483.3454088 10.1145\/3453483.3454088","DOI":"10.1145\/3453483.3454088"},{"key":"e_1_3_2_40_2","first-page":"308","article-title":"A complexity measure","volume":"4","year":"1976","unstructured":"Thomas J McCabe. 1976. A complexity measure. IEEE Transactions on software Engineering 4 (1976), 308\u2013320.","journal-title":"IEEE Transactions on software Engineering"},{"key":"e_1_3_2_41_2","unstructured":"E Meijer and Simon Peyton Jones. 1997. Henk: a typed intermediate language (types in compilation ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/henk-A-Typed-intermediate-language\/"},{"key":"e_1_3_2_42_2","first-page":"271","article-title":"Typed Closure Conversion","author":"Minamide Yasuhiko","year":"1996","unstructured":"Yasuhiko Minamide, J. Gregory Morrisett, and Robert Harper. 1996. Typed Closure Conversion. In Conference Record of POPL\u201996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996. 271\u2013283. https:\/\/doi.org\/10.1145\/237721.237791 10.1145\/237721.237791","journal-title":"Conference Record of POPL\u201996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996"},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","unstructured":"J. Gregory Morrisett David Walker Karl Crary and Neal Glew. 1998. From System F to Typed Assembly Language. In POPL \u201898 Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages San Diego CA USA January 19-21 1998 David B. MacQueen and Luca Cardelli (Eds.). ACM 85\u201397. https:\/\/doi.org\/10.1145\/268946.268954 10.1145\/268946.268954","DOI":"10.1145\/268946.268954"},{"key":"e_1_3_2_44_2","first-page":"12472","article-title":"Instead of rewriting foreign code for machine learning, automatically synthesize fast gradients","volume":"33","author":"Moses William","year":"2020","unstructured":"William Moses and Valentin Churavy. 2020. Instead of rewriting foreign code for machine learning, automatically synthesize fast gradients. Advances in neural information processing systems 33 (2020), 12472\u201312485.","journal-title":"Advances in neural information processing systems"},{"key":"e_1_3_2_45_2","first-page":"1030","article-title":"AnySeq: A High Performance Sequence Alignment Library based on Partial Evaluation","author":"M\u00fcller Andr\u00e9","year":"2020","unstructured":"Andr\u00e9 M\u00fcller, Bertil Schmidt, Andreas Hildebrandt, Richard Membarth, Roland Lei\u00dfa, Matthis Kruse, and Sebastian Hack. 2020. AnySeq: A High Performance Sequence Alignment Library based on Partial Evaluation. In 2020 IEEE International Parallel and Distributed Processing Symposium (IPDPS), New Orleans, LA, USA, May 18-22, 2020. IEEE, 1030\u20131040. https:\/\/doi.org\/10.1109\/IPDPS47924.2020.00109 10.1109\/IPDPS47924.2020.00109","journal-title":"2020 IEEE International Parallel and Distributed Processing Symposium (IPDPS), New Orleans, LA, USA, May 18-22, 2020"},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 M\u00fcller Bertil Schmidt RiChard Membarth Roland Lei\u00dfaand Sebastian Hack. 2022. AnySeq\/GPU: a novel approach for faster sequence alignment on GPUs. In ICS \u201822: 2022 International Conference on Supercomputing Virtual Event June 28 - 30 2022 Lawrence Rauchwerger Kirk W. Cameron Dimitrios S. Nikolopoulos and Dionisios N. Pnevmatikatos (Eds.). ACM 20:1\u201320:11. https:\/\/doi.org\/10.1145\/3524059.3532376 10.1145\/3524059.3532376","DOI":"10.1145\/3524059.3532376"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547637"},{"key":"e_1_3_2_48_2","unstructured":"Michael Paleczny Christopher A. Vick and Cliff Click. 2001. The Java HotSpot Server Compiler. In Proceedings of the 1st Java Virtual Machine Research and Technology Symposium April 23-24 2001 Monterey CA USA Saul Wold (Ed.). USENIX. http:\/\/www.usenix.org\/publications\/library\/proceedings\/jvm01\/paleczny.html"},{"key":"e_1_3_2_49_2","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"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/1330017.1330018"},{"key":"e_1_3_2_51_2","first-page":"228","article-title":"LAGrad: Statically Optimized Differentiable Programming in MLIR","author":"Peng Mai Jacob","year":"2023","unstructured":"Mai Jacob Peng and Christophe Dubach. 2023. LAGrad: Statically Optimized Differentiable Programming in MLIR. In Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction. 228\u2013238.","journal-title":"Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction"},{"issue":"4","key":"e_1_3_2_52_2","first-page":"40:1","article-title":"Rodent: generating renderers without writing a generator","volume":"38","author":"Membarth Richard","year":"2019","unstructured":"Ars\u00e8ne P\u00e9rard-Gayot, Richard Membarth, Roland Lei\u00dfa, Sebastian Hack, and Philipp Slusallek. 2019. Rodent: generating renderers without writing a generator. ACM Trans. Graph. 38, 4 (2019), 40:1\u201340:12. https:\/\/doi.org\/10.1145\/3306346.3322955 10.1145\/3306346.3322955","journal-title":"ACM Trans. Graph."},{"key":"e_1_3_2_53_2","first-page":"271","article-title":"Typechecking in Pure Type Systems","author":"Pollack Randy","year":"1992","unstructured":"Randy Pollack and Eric Poll. 1992. Typechecking in Pure Type Systems. In Informal proceedings of Logical Frameworks\u201992. 271\u2013288.","journal-title":"Informal proceedings of Logical Frameworks\u201992"},{"key":"e_1_3_2_54_2","unstructured":"Dragomir Radev. 2008. CLAIR collection of fraud email."},{"key":"e_1_3_2_55_2","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium Proceedings Colloque sur la Programmation Paris France April 9-11 1974 (Lecture Notes in Computer Science Vol. 19) Bernard J. Robinet (Ed.). Springer 408\u2013423. https:\/\/doi.org\/10.1007\/3-540-06859-7_148 10.1007\/3-540-06859-7_148","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000174"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1080\/10556788.2018.1435651"},{"key":"e_1_3_2_59_2","article-title":"RISE & Shine: Language-Oriented Compiler Design","author":"Steuwer Michel","year":"2022","unstructured":"Michel Steuwer, Thomas Koehler, Bastian K\u00f6pcke and Federico Pizzuti. 2022. RISE & Shine: Language-Oriented Compiler Design. CoRR abs\/2201.03611 (2022). arXiv:2201.03611 https:\/\/arxiv.org\/abs\/2201.03611","journal-title":"CoRR"},{"key":"e_1_3_2_60_2","doi-asserted-by":"crossref","unstructured":"Michel Steuwer Toomas Remmelg and Christophe Dubach. 2017. Lift: a functional data-parallel IR for high-performance GPU code generation. In Proceedings of the 2017 International Symposium on Code Generation and Optimization CGO 2017 Austin TX USA February 4-8 2017 Vijay Janapa Reddi Aaron Smith and Lingjia Tang (Eds.). ACM 74\u201385. http:\/\/dl.ACM.org\/citation.cfm?id=3049841","DOI":"10.1109\/CGO.2017.7863730"},{"key":"e_1_3_2_61_2","first-page":"256","article-title":"Dependent types and multi-monadic effects in F","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella B\u00e9guelin. 2016. Dependent types and multi-monadic effects in F. In Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM, 256\u2013270. https:\/\/doi.org\/10.1145\/2837614.2837655 10.1145\/2837614.2837655","journal-title":"Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016"},{"key":"e_1_3_2_62_2","doi-asserted-by":"crossref","unstructured":"Ross Tate Michael Stepp Zachary Tatlock and Sorin Lerner. 2009. Equality saturation: a new approach to optimization. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2009 Savannah GA USA January 21-23 2009 Zhong Shao and Benjamin C. Pierce (Eds.). ACM 264\u2013276. https:\/\/doi.org\/10.1145\/1480881.1480915 10.1145\/1480881.1480915","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_2_63_2","unstructured":"Benchmarksgame Team. 2023. The Computer Language Benchmarks Game. https:\/\/benchmarksgame-team.pages.debian.net\/benchmarksgame\/."},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003086"},{"key":"e_1_3_2_65_2","doi-asserted-by":"crossref","unstructured":"Peng Tu and David A. Padua. 1995. Efficient Building and Placing of Gating Functions. In Proceedings of the ACM SIGPLAN\u201995 Conference on Programming Language Design and Implementation (PLDI) La Jolla California USA June 18-21 1995 David W. Wall (Ed.). ACM 47\u201355. https:\/\/doi.org\/10.1145\/207110.207115 10.1145\/207110.207115","DOI":"10.1145\/207110.207115"},{"key":"e_1_3_2_66_2","first-page":"28","article-title":"The Zip Calculus","author":"Tullsen Mark","year":"2000","unstructured":"Mark Tullsen. 2000. The Zip Calculus. In Mathematics of Program Construction, 5th International Conference, MPC 2000,Ponte de Lima, Portugal, July 3-5, 2000, Proceedings. 28\u201344. https:\/\/doi.org\/10.1007\/10722010_3 10.1007\/10722010_3","journal-title":"Mathematics of Program Construction, 5th International Conference, MPC 2000,Ponte de Lima, Portugal, July 3-5, 2000, Proceedings"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_3_2_68_2","doi-asserted-by":"crossref","unstructured":"Reinhard Wilhelm Helmut Seidl and Sebastian Hack. 2013. Compiler Design - Syntactic and Semantic Analysis. Springer. https:\/\/doi.org\/10.1007\/978-3-642-17540-4 10.1007\/978-3-642-17540-4","DOI":"10.1007\/978-3-642-17540-4"},{"key":"e_1_3_2_69_2","first-page":"169","article-title":"A Dependently Typed Assembly Language","author":"Xi Hongwei","year":"2001","unstructured":"Hongwei Xi and Robert Harper. 2001. A Dependently Typed Assembly Language. In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201801), Firenze (Florence), Italy, September 3-5, 2001, Benjamin C. Pierce (Ed.). ACM, 169\u2013180. https:\/\/doi.org\/10.1145\/507635.507657 10.1145\/507635.507657","journal-title":"Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201801), Firenze (Florence), Italy, September 3-5, 2001"},{"key":"e_1_3_2_70_2","article-title":"K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs","author":"Zhao Jianhong","year":"2024","unstructured":"Jianhong Zhao, Jinhui Kang, and Yongwang Zhao. 2024. K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs. CoRR abs\/2404.18756 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2404.18756 10.48550\/ARXIV.2404.18756 arXiv:2404.18756","journal-title":"CoRR"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704840","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704840","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:17Z","timestamp":1770200057000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704840"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":69,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704840"],"URL":"https:\/\/doi.org\/10.1145\/3704840","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}