{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T13:00:08Z","timestamp":1772542808882,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":76,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,18]],"date-time":"2023-10-18T00:00:00Z","timestamp":1697587200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,18]]},"DOI":"10.1145\/3622758.3622895","type":"proceedings-article","created":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T13:41:55Z","timestamp":1697722915000},"page":"136-152","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Toward Programming Languages for Reasoning: Humans, Symbolic Systems, and AI Agents"],"prefix":"10.1145","author":[{"given":"Mark","family":"Marron","sequence":"first","affiliation":[{"name":"University of Kentucky, Lexington, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,19]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"44","author":"Allamanis Miltiadis","year":"2018","unstructured":"Miltiadis Allamanis , Earl T. Barr , Christian Bird , Premkumar T. Devanbu , Mark Marron , and Charles A. Sutton . Mining semantic loop idioms. IEEE Transactions on Software Engineering , 44 , 2018 . Miltiadis Allamanis, Earl T. Barr, Christian Bird, Premkumar T. Devanbu, Mark Marron, and Charles A. Sutton. Mining semantic loop idioms. IEEE Transactions on Software Engineering, 44, 2018.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635901"},{"key":"e_1_3_2_1_3_1","unstructured":"Async\/await 2018.    https:\/\/blogs.msdn.microsoft.com\/dsyme\/2007\/10\/10\/introducing-f-asynchronous-workflows\/. \t\t\t\t  Async\/await 2018.    https:\/\/blogs.msdn.microsoft.com\/dsyme\/2007\/10\/10\/introducing-f-asynchronous-workflows\/."},{"key":"e_1_3_2_1_4_1","volume-title":"ICSE","author":"Atlidakis Vaggelis","year":"2019","unstructured":"Vaggelis Atlidakis , Patrice Godefroid , and Marina Polishchuk . Restler : Stateful REST API fuzzing . In ICSE , 2019 . Vaggelis Atlidakis, Patrice Godefroid, and Marina Polishchuk. Restler: Stateful REST API fuzzing. In ICSE, 2019."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442529"},{"key":"e_1_3_2_1_6_1","volume-title":"The essence of data access in C\u03c9: The power is in the dot!  In ECOOP","author":"Bierman Gavin","year":"2005","unstructured":"Gavin Bierman , Erik Meijer , and Wolfram Schulte . The essence of data access in C\u03c9: The power is in the dot! In ECOOP , 2005 . Gavin Bierman, Erik Meijer, and Wolfram Schulte. The essence of data access in C\u03c9: The power is in the dot! In ECOOP, 2005."},{"key":"e_1_3_2_1_7_1","volume-title":"OOPSLA","author":"Stephen","year":"2003","unstructured":"Stephen M. Blackburn and Kathryn S. McKinley. Ulterior reference counting: Fast garbage collection without a long wait . In OOPSLA , 2003 . Stephen M. Blackburn and Kathryn S. McKinley. Ulterior reference counting: Fast garbage collection without a long wait. In OOPSLA, 2003."},{"key":"e_1_3_2_1_8_1","volume-title":"Racerd: Compositional static race detection","author":"Blackshear Sam","year":"2018","unstructured":"Sam Blackshear , Nikos Gorogiannis , Peter W. O\u2019Hearn , and Ilya Sergey . Racerd: Compositional static race detection . 2018 . Sam Blackshear, Nikos Gorogiannis, Peter W. O\u2019Hearn, and Ilya Sergey. Racerd: Compositional static race detection. 2018."},{"key":"e_1_3_2_1_9_1","first-page":"20","author":"Brooks Frederick P.","year":"1987","unstructured":"Frederick P. Brooks , Jr. No silver bullet essence and accidents of software engineering. Computer , 20 , 1987 . Frederick P. Brooks, Jr. No silver bullet essence and accidents of software engineering. Computer, 20, 1987.","journal-title":"Computer"},{"key":"e_1_3_2_1_10_1","first-page":"5","author":"Burckhardt Sebastian","year":"2021","unstructured":"Sebastian Burckhardt , Chris Gillum , David Justo , Konstantinos Kallas , Connor McMahon , and Christopher S. Meiklejohn . Durable functions: Semantics for stateful serverless. Proceedings ACM Programming Languages , 5 , 2021 . Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, and Christopher S. Meiklejohn. Durable functions: Semantics for stateful serverless. Proceedings ACM Programming Languages, 5, 2021.","journal-title":"Proceedings ACM Programming Languages"},{"key":"e_1_3_2_1_11_1","unstructured":"V8 doesn\u2019t stable sort 2018.  https:\/\/bugs.chromium.org\/p\/v8\/issues\/detail?id=90. \t\t\t\t  V8 doesn\u2019t stable sort 2018.  https:\/\/bugs.chromium.org\/p\/v8\/issues\/detail?id=90."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037754"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582447"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_2_1_15_1","unstructured":"Copilot 2023.  https:\/\/github.com\/features\/copilot. \t\t\t\t  Copilot 2023.  https:\/\/github.com\/features\/copilot."},{"key":"e_1_3_2_1_16_1","first-page":"13","author":"Cytron Ron","year":"1991","unstructured":"Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , and F. Kenneth Zadeck . Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Language Systems , 13 , 1991 . Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Language Systems, 13, 1991.","journal-title":"ACM Transactions on Programming Language Systems"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1243380"},{"key":"e_1_3_2_1_18_1","volume-title":"Z3 SMT Theorem Prover.  https:\/\/github.com\/Z3Prover\/z3","author":"de Moura Leonardo","year":"2021","unstructured":"Leonardo de Moura , Nikolaj Bj\u00f8rner , and et. al. Z3 SMT Theorem Prover. https:\/\/github.com\/Z3Prover\/z3 , 2021 . Leonardo de Moura, Nikolaj Bj\u00f8rner, and et. al. Z3 SMT Theorem Prover. https:\/\/github.com\/Z3Prover\/z3, 2021."},{"key":"e_1_3_2_1_19_1","unstructured":"Azure durable functions 2019.    https:\/\/docs.microsoft.com\/en-us\/azure\/azure-functions\/durable\/durable-functions-overview. \t\t\t\t  Azure durable functions 2019.    https:\/\/docs.microsoft.com\/en-us\/azure\/azure-functions\/durable\/durable-functions-overview."},{"key":"e_1_3_2_1_20_1","unstructured":"express.js 2019.  https:\/\/expressjs.com\/. \t\t\t\t  express.js 2019.  https:\/\/expressjs.com\/."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949332"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297052"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2588555.2612177"},{"key":"e_1_3_2_1_28_1","volume-title":"HotOS XIV","author":"Guo Zhenyu","year":"2013","unstructured":"Zhenyu Guo , Sean McDirmid , Mao Yang , Li Zhuang , Pu Zhang , Yingwei Luo , Tom Bergan , Madan Musuvathi , Zheng Zhang , and Lidong Zhou . Failure recovery : When the cure is worse than the disease . In HotOS XIV , 2013 . Zhenyu Guo, Sean McDirmid, Mao Yang, Li Zhuang, Pu Zhang, Yingwei Luo, Tom Bergan, Madan Musuvathi, Zheng Zhang, and Lidong Zhou. Failure recovery: When the cure is worse than the disease. In HotOS XIV, 2013."},{"key":"e_1_3_2_1_29_1","volume-title":"CAV","author":"Gupta Ashutosh","year":"2009","unstructured":"Ashutosh Gupta and Andrey Rybalchenko . Invgen : An efficient invariant generator . In CAV , 2009 . Ashutosh Gupta and Andrey Rybalchenko. Invgen: An efficient invariant generator. In CAV, 2009."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2190025.2190075"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"e_1_3_2_1_32_1","first-page":"12","author":"Hoare C. A. R.","year":"1969","unstructured":"C. A. R. Hoare . An axiomatic basis for computer programming. Communications of the ACM , 12 , 1969 . C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12, 1969.","journal-title":"Communications of the ACM"},{"key":"e_1_3_2_1_33_1","first-page":"39","author":"Hovemeyer David","year":"2004","unstructured":"David Hovemeyer and William Pugh . Finding bugs is easy. SIGPLAN Notices , 39 , 2004 . David Hovemeyer and William Pugh. Finding bugs is easy. SIGPLAN Notices, 39, 2004.","journal-title":"SIGPLAN Notices"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/229000.226322"},{"key":"e_1_3_2_1_35_1","unstructured":"Java streams 2019.    https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/stream\/package-summary.html. \t\t\t\t  Java streams 2019.    https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/stream\/package-summary.html."},{"key":"e_1_3_2_1_36_1","unstructured":"On partially-constructed objects 2010.    http:\/\/joeduffyblog.com\/2010\/06\/27\/on-partiallyconstructed-objects\/. \t\t\t\t  On partially-constructed objects 2010.    http:\/\/joeduffyblog.com\/2010\/06\/27\/on-partiallyconstructed-objects\/."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11490-4_24"},{"key":"e_1_3_2_1_38_1","volume-title":"Optimizing Compilers for Modern Architectures: A  Dependence-based Approach","author":"Kennedy Ken","year":"2002","unstructured":"Ken Kennedy and John R. Allen . Optimizing Compilers for Modern Architectures: A Dependence-based Approach . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA, 2002 . Ken Kennedy and John R. Allen. Optimizing Compilers for Modern Architectures: A Dependence-based Approach. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2002."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869470"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250766"},{"key":"e_1_3_2_1_42_1","volume-title":"APLAS","author":"K. Rustan","year":"2005","unstructured":"K. Rustan M. Leino and Francesco Logozzo. Loop invariants on demand . In APLAS , 2005 . K. Rustan M. Leino and Francesco Logozzo. Loop invariants on demand. In APLAS, 2005."},{"key":"e_1_3_2_1_43_1","first-page":"43","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy . A formally verified compiler back-end. Journal Automated Reasoning , 43 , 2009 . Xavier Leroy. A formally verified compiler back-end. Journal Automated Reasoning, 43, 2009.","journal-title":"Journal Automated Reasoning"},{"key":"e_1_3_2_1_44_1","unstructured":"LINQ 2019.    https:\/\/docs.microsoft.com\/en-us\/dotnet\/csharp\/programming-guide\/concepts\/linq\/. \t\t\t\t  LINQ 2019.    https:\/\/docs.microsoft.com\/en-us\/dotnet\/csharp\/programming-guide\/concepts\/linq\/."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/800233.807045"},{"key":"e_1_3_2_1_46_1","unstructured":"lodash 2019.  https:\/\/lodash.com\/. \t\t\t\t  lodash 2019.  https:\/\/lodash.com\/."},{"key":"e_1_3_2_1_47_1","unstructured":"log4j CVE 2021.  https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2021-44228. \t\t\t\t  log4j CVE 2021.  https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2021-44228."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807442.2807459"},{"key":"e_1_3_2_1_49_1","first-page":"1","author":"Mazinanian Davood","year":"2017","unstructured":"Davood Mazinanian , Ameya Ketkar , Nikolaos Tsantalis , and Danny Dig . Understanding the use of lambda expressions in Java. Proceedings ACM Programming Languages , 1 , 2017 . Davood Mazinanian, Ameya Ketkar, Nikolaos Tsantalis, and Danny Dig. Understanding the use of lambda expressions in Java. Proceedings ACM Programming Languages, 1, 2017.","journal-title":"Java. Proceedings ACM Programming Languages"},{"key":"e_1_3_2_1_50_1","volume-title":"Edinburgh University  Press","author":"McCarthy John","year":"1969","unstructured":"John McCarthy and Patrick J. Hayes . Some philosophical problems from the standpoint of artificial intelligence. In Machine Intelligence 4, pages 463\u2013502 . Edinburgh University Press , 1969 . John McCarthy and Patrick J. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In Machine Intelligence 4, pages 463\u2013502. Edinburgh University Press, 1969."},{"key":"e_1_3_2_1_51_1","volume-title":"Code Complete","author":"McConnell Steve","year":"2004","unstructured":"Steve McConnell . Code Complete , Second Edition. Microsoft Press , Redmond, WA, USA , 2004 . Steve McConnell. Code Complete, Second Edition. Microsoft Press, Redmond, WA, USA, 2004."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869495"},{"key":"e_1_3_2_1_53_1","first-page":"14","author":"Milanova Ana","year":"2005","unstructured":"Ana Milanova , Atanas Rountev , and Barbara G. Ryder . Parameterized object sensitivity for points-to analysis for Java. ACM Transactions on Software Engineering and Methodology , 14 , 2005 . Ana Milanova, Atanas Rountev, and Barbara G. Ryder. Parameterized object sensitivity for points-to analysis for Java. ACM Transactions on Software Engineering and Methodology, 14, 2005.","journal-title":"Java. ACM Transactions on Software Engineering and Methodology"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_3_2_1_55_1","volume-title":"Advanced Compiler Design and Implementation","author":"Muchnick Steven S.","year":"1997","unstructured":"Steven S. Muchnick . Advanced Compiler Design and Implementation . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA, 1997 . Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1997."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/374262"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2986012.2986031"},{"key":"e_1_3_2_1_59_1","unstructured":"npm.js 2023.  https:\/\/www.npmjs.com\/. \t\t\t\t  npm.js 2023.  https:\/\/www.npmjs.com\/."},{"key":"e_1_3_2_1_60_1","volume-title":"POPL","author":"O\u2019Hearn Peter W.","year":"2019","unstructured":"Peter W. O\u2019Hearn . Incorrectness logic . In POPL , 2019 . Peter W. O\u2019Hearn. Incorrectness logic. In POPL, 2019."},{"key":"e_1_3_2_1_61_1","volume-title":"GPT-4 technical report","author":"AI.","year":"2023","unstructured":"Open AI. GPT-4 technical report , 2023 . OpenAI. GPT-4 technical report, 2023."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594297"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375587"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_1_65_1","unstructured":"react 2019.  https:\/\/reactjs.org\/. \t\t\t\t  react 2019.  https:\/\/reactjs.org\/."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_67_1","unstructured":"Rust 2022.  https:\/\/www.rust-lang.org\/. \t\t\t\t  Rust 2022.  https:\/\/www.rust-lang.org\/."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_1_69_1","unstructured":"Semantic versioning 2.0.0 2018.  https:\/\/semver.org\/. \t\t\t\t  Semantic versioning 2.0.0 2018.  https:\/\/semver.org\/."},{"key":"e_1_3_2_1_70_1","first-page":"7762","volume-title":"Advances in Neural Information Processing Systems 31","author":"Si Xujie","unstructured":"Xujie Si , Hanjun Dai , Mukund Raghothaman , Mayur Naik , and Le Song . Learning loop invariants for program verification . In Advances in Neural Information Processing Systems 31 , pages 7751\u2013 7762 . 2018. Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. Learning loop invariants for program verification. In Advances in Neural Information Processing Systems 31, pages 7751\u20137762. 2018."},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_14"},{"key":"e_1_3_2_1_73_1","volume-title":"POPL","author":"Jesse","year":"2011","unstructured":"Jesse A. Tov and Riccardo Pucella. Practical affine types . In POPL , 2011 . Jesse A. Tov and Riccardo Pucella. Practical affine types. In POPL, 2011."},{"key":"e_1_3_2_1_74_1","unstructured":"3\n   .3 2019.  https:\/\/www.typescriptlang.org\/. \t\t\t\t  3.3 2019.  https:\/\/www.typescriptlang.org\/."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_22"},{"key":"e_1_3_2_1_76_1","volume-title":"Linear types can change the world!  In Programming Concepts and Methods","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . Linear types can change the world! In Programming Concepts and Methods , 1990 . Philip Wadler. Linear types can change the world! In Programming Concepts and Methods, 1990."},{"key":"e_1_3_2_1_77_1","volume-title":"PLDI","author":"Zhao Wenyu","year":"2022","unstructured":"Wenyu Zhao , Stephen M. Blackburn , and Kathryn S . McKinley. Low-latency, high-throughput garbage collection . In PLDI , 2022 . Wenyu Zhao, Stephen M. Blackburn, and Kathryn S. McKinley. Low-latency, high-throughput garbage collection. In PLDI, 2022."}],"event":{"name":"Onward! '23: 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software","location":"Cascais Portugal","acronym":"Onward! '23","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622758.3622895","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622758.3622895","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:45:23Z","timestamp":1750268723000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622758.3622895"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,18]]},"references-count":76,"alternative-id":["10.1145\/3622758.3622895","10.1145\/3622758"],"URL":"https:\/\/doi.org\/10.1145\/3622758.3622895","relation":{},"subject":[],"published":{"date-parts":[[2023,10,18]]},"assertion":[{"value":"2023-10-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}