{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:50Z","timestamp":1750219790959,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T00:00:00Z","timestamp":1689120000000},"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":[],"published-print":{"date-parts":[[2023,7,12]]},"DOI":"10.1145\/3597926.3605239","type":"proceedings-article","created":{"date-parts":[[2023,7,13]],"date-time":"2023-07-13T20:12:53Z","timestamp":1689279173000},"page":"1552-1554","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning about MLIR Semantics through Effects and Handlers"],"prefix":"10.1145","author":[{"given":"Pingshi","family":"Yu","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2023. GCC online documentation. https:\/\/gcc.gnu.org\/onlinedocs\/ \t\t\t\t  2023. GCC online documentation. https:\/\/gcc.gnu.org\/onlinedocs\/"},{"key":"e_1_3_2_1_2_1","unstructured":"2023. GHC.Core. https:\/\/downloads.haskell. org\/ghc\/9.0.1\/docs\/html\/libraries\/ ghc-9.0.1\/GHC-Core.html \t\t\t\t  2023. GHC.Core. https:\/\/downloads.haskell. org\/ghc\/9.0.1\/docs\/html\/libraries\/ ghc-9.0.1\/GHC-Core.html"},{"key":"e_1_3_2_1_3_1","unstructured":"2023. 'linalg' Dialect-MLIR. https:\/\/mlir.llvm.org\/docs\/Dialects\/Linalg\/\/ \t\t\t\t  2023. 'linalg' Dialect-MLIR. https:\/\/mlir.llvm.org\/docs\/Dialects\/Linalg\/\/"},{"key":"e_1_3_2_1_4_1","unstructured":"2023. 'memref' Dialect-MLIR. https:\/\/mlir.llvm.org\/docs\/Dialects\/MemRef\/ \t\t\t\t  2023. 'memref' Dialect-MLIR. https:\/\/mlir.llvm.org\/docs\/Dialects\/MemRef\/"},{"key":"e_1_3_2_1_5_1","unstructured":"2023. The MIR (Mid-level IR). https:\/\/rustc-dev-guide.rust-lang.org\/mir\/index. html \t\t\t\t  2023. The MIR (Mid-level IR). https:\/\/rustc-dev-guide.rust-lang.org\/mir\/index. html"},{"key":"e_1_3_2_1_6_1","unstructured":"2023. mlir-lean: embedded MLIR in LEAN. https:\/\/github.com\/opencompl\/leanmlir \t\t\t\t  2023. mlir-lean: embedded MLIR in LEAN. https:\/\/github.com\/opencompl\/leanmlir"},{"key":"e_1_3_2_1_7_1","unstructured":"2023. Traits-MLIR. https:\/\/mlir.llvm.org\/docs\/Traits\/ \t\t\t\t  2023. Traits-MLIR. https:\/\/mlir.llvm.org\/docs\/Traits\/"},{"key":"e_1_3_2_1_8_1","volume-title":"Ho Young Jhoo, and Juneyoung Lee","author":"Bang Seongwon","year":"2022","unstructured":"Seongwon Bang , Seunghyeon Nam , Inwhan Chun , Ho Young Jhoo, and Juneyoung Lee . 2022 . SMT-Based Translation Validation for Machine Learning Compiler. In Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Springer, 386-407. Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, and Juneyoung Lee. 2022. SMT-Based Translation Validation for Machine Learning Compiler. In Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Springer, 386-407."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25","author":"de Moura Leonardo","year":"2015","unstructured":"Leonardo de Moura , Soonho Kong , Jeremy Avigad , Floris Van Doorn , and Jakob von Raumer . 2015 . The Lean theorem prover (system description) . In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25 . Springer , 378 - 388 . Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25. Springer, 378-388."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the ACM on Programming Languages 1, OOPSLA ( 2017 ), 1-29","author":"Donaldson Alastair F","year":"2017","unstructured":"Alastair F Donaldson , Hugues Evrard , Andrei Lascu , and Paul Thomson . 2017 . Automated testing of graphics shader compilers . Proceedings of the ACM on Programming Languages 1, OOPSLA ( 2017 ), 1-29 . Alastair F Donaldson, Hugues Evrard, Andrei Lascu, and Paul Thomson. 2017. Automated testing of graphics shader compilers. Proceedings of the ACM on Programming Languages 1, OOPSLA ( 2017 ), 1-29."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the ACM on Programming Languages 5, OOPSLA ( 2021 ), 1-28","author":"Iorga Dan","year":"2021","unstructured":"Dan Iorga , Alastair F Donaldson , Tyler Sorensen , and John Wickerson . 2021 . The semantics of shared memory in Intel CPU\/FPGA systems . Proceedings of the ACM on Programming Languages 5, OOPSLA ( 2021 ), 1-28 . Dan Iorga, Alastair F Donaldson, Tyler Sorensen, and John Wickerson. 2021. The semantics of shared memory in Intel CPU\/FPGA systems. Proceedings of the ACM on Programming Languages 5, OOPSLA ( 2021 ), 1-28."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Oleg Kiselyov Amr Sabry and Cameron Swords. 2013. Extensible efects: an alternative to monad transformers. ACM SIGPLAN Notices 48 12 ( 2013 ) 59-70. \t\t\t\t  Oleg Kiselyov Amr Sabry and Cameron Swords. 2013. Extensible efects: an alternative to monad transformers. ACM SIGPLAN Notices 48 12 ( 2013 ) 59-70.","DOI":"10.1145\/2578854.2503791"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the ACM on Programming Languages 7, POPL ( 2023 ), 1740-1769","author":"Klimis Vasileios","year":"2023","unstructured":"Vasileios Klimis , Jack Clark , Alan Baker , David Neto , John Wickerson , and Alastair F Donaldson . 2023 . Taking Back Control in an Intermediate Representation for GPU Computing . Proceedings of the ACM on Programming Languages 7, POPL ( 2023 ), 1740-1769 . Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F Donaldson. 2023. Taking Back Control in an Intermediate Representation for GPU Computing. Proceedings of the ACM on Programming Languages 7, POPL ( 2023 ), 1740-1769."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Vu Le Mehrdad Afshari and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. ACM Sigplan Notices 49 6 ( 2014 ) 216-226. \t\t\t\t  Vu Le Mehrdad Afshari and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. ACM Sigplan Notices 49 6 ( 2014 ) 216-226.","DOI":"10.1145\/2666356.2594334"},{"key":"e_1_3_2_1_16_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy , Sandrine Blazy , Daniel K\u00e4stner , Bernhard Schommer , Markus Pister , and Christian Ferdinand . 2016 . CompCert-a formally verified optimizing compiler . In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_3_2_1_18_1","volume-title":"Programming Languages and Systems: 18th European Symposium on Programming, ESOP","author":"Plotkin Gordon","year":"2009","unstructured":"Gordon Plotkin and Matija Pretnar . 2009. Handlers of algebraic efects . In Programming Languages and Systems: 18th European Symposium on Programming, ESOP 2009 , Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings 18. Springer , 80-94. Gordon Plotkin and Matija Pretnar. 2009. Handlers of algebraic efects. In Programming Languages and Systems: 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings 18. Springer, 80-94."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_3_2_1_20_1","first-page":"302","volume-title":"Mathematics of Program Construction: 12th International Conference, MPC 2015, K\u00f6nigswinter, Germany, June 29-July 1, 2015. Proceedings 12","author":"Wu Nicolas","year":"2015","unstructured":"Nicolas Wu and Tom Schrijvers . 2015 . Fusion for free: Eficient algebraic efect handlers . In Mathematics of Program Construction: 12th International Conference, MPC 2015, K\u00f6nigswinter, Germany, June 29-July 1, 2015. Proceedings 12 . Springer , 302 - 322 . Nicolas Wu and Tom Schrijvers. 2015. Fusion for free: Eficient algebraic efect handlers. In Mathematics of Program Construction: 12th International Conference, MPC 2015, K\u00f6nigswinter, Germany, June 29-July 1, 2015. Proceedings 12. Springer, 302-322."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_3_2_1_22_1","volume-title":"Interaction trees: representing recursive and impure programs in Coq. arXiv preprint arXiv","author":"Zakowski Yannick","year":"1906","unstructured":"Li-yao Xia, Yannick Zakowski , Paul He , Chung-Kil Hur , Gregory Malecha , Benjamin C Pierce , and Steve Zdancewic . 2019. Interaction trees: representing recursive and impure programs in Coq. arXiv preprint arXiv : 1906 . 00046 ( 2019 ). Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C Pierce, and Steve Zdancewic. 2019. Interaction trees: representing recursive and impure programs in Coq. arXiv preprint arXiv: 1906. 00046 ( 2019 )."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the ACM on Programming Languages 5, ICFP ( 2021 ), 1-29","author":"Yang Zhixuan","year":"2021","unstructured":"Zhixuan Yang and Nicolas Wu . 2021 . Reasoning about efect interaction by fusion . Proceedings of the ACM on Programming Languages 5, ICFP ( 2021 ), 1-29 . Zhixuan Yang and Nicolas Wu. 2021. Reasoning about efect interaction by fusion. Proceedings of the ACM on Programming Languages 5, ICFP ( 2021 ), 1-29."},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the ACM on Programming Languages 5, ICFP ( 2021 ), 1-30","author":"Zakowski Yannick","year":"2021","unstructured":"Yannick Zakowski , Calvin Beck , Irene Yoon , Ilia Zaichuk , Vadim Zaliva , and Steve Zdancewic . 2021 . Modular, compositional, and executable formal semantics for LLVM IR . Proceedings of the ACM on Programming Languages 5, ICFP ( 2021 ), 1-30 . Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. 2021. Modular, compositional, and executable formal semantics for LLVM IR. Proceedings of the ACM on Programming Languages 5, ICFP ( 2021 ), 1-30."}],"event":{"name":"ISSTA '23: 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"],"location":"Seattle WA USA","acronym":"ISSTA '23"},"container-title":["Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597926.3605239","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3597926.3605239","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:59Z","timestamp":1750178279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597926.3605239"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,12]]},"references-count":24,"alternative-id":["10.1145\/3597926.3605239","10.1145\/3597926"],"URL":"https:\/\/doi.org\/10.1145\/3597926.3605239","relation":{},"subject":[],"published":{"date-parts":[[2023,7,12]]},"assertion":[{"value":"2023-07-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}