{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:14:33Z","timestamp":1767928473458,"version":"3.49.0"},"reference-count":79,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"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":[[2023,10,16]]},"abstract":"<jats:p>\n            Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact\n            <jats:italic>complete<\/jats:italic>\n            for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.\n          <\/jats:p>","DOI":"10.1145\/3622835","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1063-1092","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Complete First-Order Reasoning for Properties of Functional Programs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"first","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1898-439X","authenticated-orcid":false,"given":"Lucas","family":"Pe\u00f1a","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California San Diego, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-721X","authenticated-orcid":false,"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Computing with an SMT Solver","author":"Amin Nada","unstructured":"Nada Amin , K. Rustan M. Leino , and Tiark Rompf . 2014. Computing with an SMT Solver . In Tests and Proofs, Martina Seidl and Nikolai Tillmann (Eds.). Springer International Publishing , Cham . 20\u201335. isbn:978-3-319-09099-3 Nada Amin, K. Rustan M. Leino, and Tiark Rompf. 2014. Computing with an SMT Solver. In Tests and Proofs, Martina Seidl and Nikolai Tillmann (Eds.). Springer International Publishing, Cham. 20\u201335. isbn:978-3-319-09099-3"},{"key":"e_1_2_1_2_1","volume-title":"Automated Deduction \u2013 CADE-20","author":"Baader Franz","year":"1864","unstructured":"Franz Baader and Silvio Ghilardi . 2005. Connecting Many-Sorted Theories . In Automated Deduction \u2013 CADE-20 , Robert Nieuwenhuis (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 278\u2013294. isbn:978-3-540-3 1864 -4 Franz Baader and Silvio Ghilardi. 2005. Connecting Many-Sorted Theories. In Automated Deduction \u2013 CADE-20, Robert Nieuwenhuis (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 278\u2013294. isbn:978-3-540-31864-4"},{"key":"e_1_2_1_3_1","volume-title":"CVC4","author":"Barrett Clark","unstructured":"Clark Barrett , Christopher L. Conway , Morgan Deters , Liana Hadarean , Dejan Jovanovi\u0107 , Tim King , Andrew Reynolds , and Cesare Tinelli . 2011. CVC4 . In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 171\u2013177. isbn:978-3-642-22110-1 Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 171\u2013177. isbn:978-3-642-22110-1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_1_5_1","volume-title":"Handbook of Mathematical Logic","author":"Barwise Jon","unstructured":"Jon Barwise . 1977. Handbook of Mathematical Logic . North-Holland Publishing Company , Amsterdam . Jon Barwise. 1977. Handbook of Mathematical Logic. North-Holland Publishing Company, Amsterdam."},{"key":"e_1_2_1_6_1","volume-title":"Integrating Decision Procedures for Temporal Verification. Ph. D. Dissertation","author":"Bjorner Nikolaj Skallerud","unstructured":"Nikolaj Skallerud Bjorner . 1999. Integrating Decision Procedures for Temporal Verification. Ph. D. Dissertation . Stanford University . Stanford, CA, USA. isbn:0599239840 AAI9924398 Nikolaj Skallerud Bjorner. 1999. Integrating Decision Procedures for Temporal Verification. Ph. D. Dissertation. Stanford University. Stanford, CA, USA. isbn:0599239840 AAI9924398"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"e_1_2_1_8_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, Christian G","author":"Blanchette Jasmin Christian","unstructured":"Jasmin Christian Blanchette and Koen Claessen . 2010. Generating Counterexamples for Structural Inductions by\u00a0Exploiting Nonstandard Models . In Logic for Programming, Artificial Intelligence, and Reasoning, Christian G . Ferm\u00fcller and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg . 127\u2013141. isbn:978-3-642-16242-8 Jasmin Christian Blanchette and Koen Claessen. 2010. Generating Counterexamples for Structural Inductions by\u00a0Exploiting Nonstandard Models. In Logic for Programming, Artificial Intelligence, and Reasoning, Christian G. Ferm\u00fcller and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 127\u2013141. isbn:978-3-642-16242-8"},{"key":"e_1_2_1_9_1","unstructured":"Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. HAL-Inria Wroclaw Poland. 53\u201364. https:\/\/hal.inria.fr\/hal-00790310 \t\t\t\t  Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. HAL-Inria Wroclaw Poland. 53\u201364. https:\/\/hal.inria.fr\/hal-00790310"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0314-5"},{"key":"e_1_2_1_11_1","volume-title":"A Computational Logic Handbook","author":"Boyer Robert S.","unstructured":"Robert S. Boyer and J. Strother Moore . 1988. A Computational Logic Handbook . Academic Press Professional, Inc. , USA. isbn:0121229521 Robert S. Boyer and J. Strother Moore. 1988. A Computational Logic Handbook. Academic Press Professional, Inc., USA. isbn:0121229521"},{"key":"e_1_2_1_12_1","volume-title":"Bradley and Zohar Manna","author":"Aaron","year":"2007","unstructured":"Aaron R. Bradley and Zohar Manna . 2007 . The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag , Berlin, Heidelberg. isbn:3540741127 Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, Berlin, Heidelberg. isbn:3540741127"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Harsh Raju Chamarthi Peter Dillinger Panagiotis Manolios and Daron Vroon. 2011. The ACL2 Sedan Theorem Proving System. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Part of the Joint European Conferences on Theory and Practice of Software (TACAS\u201911\/ETAPS\u201911). Springer-Verlag Berlin Heidelberg. 291\u2013295. isbn:9783642198342 \t\t\t\t  Harsh Raju Chamarthi Peter Dillinger Panagiotis Manolios and Daron Vroon. 2011. The ACL2 Sedan Theorem Proving System. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Part of the Joint European Conferences on Theory and Practice of Software (TACAS\u201911\/ETAPS\u201911). Springer-Verlag Berlin Heidelberg. 291\u2013295. isbn:9783642198342","DOI":"10.1007\/978-3-642-19835-9_27"},{"key":"e_1_2_1_14_1","volume-title":"Automated Deduction \u2013 CADE-24","author":"Claessen Koen","unstructured":"Koen Claessen , Moa Johansson , Dan Ros\u00e9n , and Nicholas Smallbone . 2013. Automating Inductive Proofs Using Theory Exploration . In Automated Deduction \u2013 CADE-24 , Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 392\u2013406. isbn:978-3-642-38574-2 Koen Claessen, Moa Johansson, Dan Ros\u00e9n, and Nicholas Smallbone. 2013. Automating Inductive Proofs Using Theory Exploration. In Automated Deduction \u2013 CADE-24, Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 392\u2013406. isbn:978-3-642-38574-2"},{"key":"e_1_2_1_15_1","volume-title":"Frontiers of Combining Systems","author":"Cruanes Simon","unstructured":"Simon Cruanes . 2017. Superposition with Structural Induction . In Frontiers of Combining Systems , Clare Dixon and Marcelo Finger (Eds.). Springer International Publishing , Cham . 172\u2013188. isbn:978-3-319-66167-4 Simon Cruanes. 2017. Superposition with Structural Induction. In Frontiers of Combining Systems, Clare Dixon and Marcelo Finger (Eds.). Springer International Publishing, Cham. 172\u2013188. isbn:978-3-319-66167-4"},{"key":"e_1_2_1_16_1","unstructured":"The dafny-lang community. 2022. https:\/\/dafny-lang.github.io\/dafny\/DafnyRef\/DafnyRef \t\t\t\t  The dafny-lang community. 2022. https:\/\/dafny-lang.github.io\/dafny\/DafnyRef\/DafnyRef"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000157"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_20_1","volume-title":"A mathematical introduction to logic","author":"Enderton Herbert B.","unstructured":"Herbert B. Enderton . 1972. A mathematical introduction to logic . Academic Press , New York . Herbert B. Enderton. 1972. A mathematical introduction to logic. Academic Press, New York."},{"key":"e_1_2_1_21_1","volume-title":"Why3 \u2014 Where Programs Meet Provers","author":"Filli\u00e2tre Jean-Christophe","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich . 2013. Why3 \u2014 Where Programs Meet Provers . In Programming Languages and Systems, Matthias Felleisen and Philippa Gardner (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 125\u2013128. isbn:978-3-642-37036-6 Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 \u2014 Where Programs Meet Provers. In Programming Languages and Systems, Matthias Felleisen and Philippa Gardner (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 125\u2013128. isbn:978-3-642-37036-6"},{"key":"e_1_2_1_22_1","volume-title":"Combinations of Theories and the Bernays-Sch\u00f6nfinkel-Ramsey Class. In 4th International Verification Workshop - VERIFY\u201907","volume":"54","author":"Fontaine Pascal","year":"2007","unstructured":"Pascal Fontaine . 2007 . Combinations of Theories and the Bernays-Sch\u00f6nfinkel-Ramsey Class. In 4th International Verification Workshop - VERIFY\u201907 , Bernhard Beckert (Ed.) (CEUR Workshop Proceedings , Vol. 259). HAL-Inria, Bremen, Germany. 37\u2013 54 . https:\/\/hal.inria.fr\/inria-00186639 URL : http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-259\/paper06.pdf Pascal Fontaine. 2007. Combinations of Theories and the Bernays-Sch\u00f6nfinkel-Ramsey Class. In 4th International Verification Workshop - VERIFY\u201907, Bernhard Beckert (Ed.) (CEUR Workshop Proceedings, Vol. 259). HAL-Inria, Bremen, Germany. 37\u201354. https:\/\/hal.inria.fr\/inria-00186639 URL : http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-259\/paper06.pdf"},{"key":"e_1_2_1_23_1","volume-title":"Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories","author":"Ge Yeting","unstructured":"Yeting Ge and Leonardo de Moura . 2009. Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories . In Computer Aided Verification, Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 306\u2013320. isbn:978-3-642-02658-4 Yeting Ge and Leonardo de Moura. 2009. Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In Computer Aided Verification, Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 306\u2013320. isbn:978-3-642-02658-4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"e_1_2_1_25_1","volume-title":"Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.)","author":"Haifani Fajar","unstructured":"Fajar Haifani , Sophie Tourret , and Christoph Weidenbach . 2021. Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance . In Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.) . Springer International Publishing , Cham . 327\u2013343. isbn:978-3-030-79876-5 Fajar Haifani, Sophie Tourret, and Christoph Weidenbach. 2021. Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. In Automated Deduction \u2013 CADE 28, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham. 327\u2013343. isbn:978-3-030-79876-5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_34"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360592"},{"key":"e_1_2_1_29_1","volume-title":"A Shorter Model Theory","author":"Hodges Wilfrid","unstructured":"Wilfrid Hodges . 1997. A Shorter Model Theory . Cambridge University Press , USA. isbn:0521587131 Wilfrid Hodges. 1997. A Shorter Model Theory. Cambridge University Press, USA. isbn:0521587131"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2017.00033"},{"key":"e_1_2_1_31_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Ihlemann Carsten","unstructured":"Carsten Ihlemann , Swen Jacobs , and Viorica Sofronie-Stokkermans . 2008. On Local Reasoning in Verification . In Tools and Algorithms for the Construction and Analysis of Systems , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 265\u2013281. isbn:978-3-540-78800-3 Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans. 2008. On Local Reasoning in Verification. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 265\u2013281. isbn:978-3-540-78800-3"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-1675-3_3"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_21"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181789"},{"key":"e_1_2_1_35_1","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann Matt","unstructured":"Matt Kaufmann , J. Strother Moore , and Panagiotis Manolios . 2000. Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers , USA. isbn:0792377443 Matt Kaufmann, J. Strother Moore, and Panagiotis Manolios. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, USA. isbn:0792377443"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009887"},{"key":"e_1_2_1_37_1","volume-title":"First-Order Theorem Proving and Vampire","author":"Kov\u00e1cs Laura","unstructured":"Laura Kov\u00e1cs and Andrei Voronkov . 2013. First-Order Theorem Proving and Vampire . In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 1\u201335. isbn:978-3-642-39799-8 Laura Kov\u00e1cs and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201335. isbn:978-3-642-39799-8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763569"},{"key":"e_1_2_1_39_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. June https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/ \t\t\t\t  K. Rustan M. Leino. 2008. This is Boogie 2. June https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_1_41_1","volume-title":"Trigger Selection Strategies to Stabilize Program Verifiers","author":"Leino K. R. M.","unstructured":"K. R. M. Leino and Cl\u00e9ment Pit-Claudel . 2016. Trigger Selection Strategies to Stabilize Program Verifiers . In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing , Cham . 361\u2013381. isbn:978-3-319-41528-4 K. R. M. Leino and Cl\u00e9ment Pit-Claudel. 2016. Trigger Selection Strategies to Stabilize Program Verifiers. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham. 361\u2013381. isbn:978-3-319-41528-4"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Rustan Leino and Nadia Polikarpova. 2013. Verified Calculations. https:\/\/www.microsoft.com\/en-us\/research\/publication\/verified-calculations\/ \t\t\t\t  Rustan Leino and Nadia Polikarpova. 2013. Verified Calculations. https:\/\/www.microsoft.com\/en-us\/research\/publication\/verified-calculations\/","DOI":"10.1007\/978-3-642-54108-7_9"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_2_1_44_1","first-page":"729","article-title":"Axiomatizable classes of locally free algebras of certain types","volume":"3","author":"Mal\u2019tsev A. I.","year":"1962","unstructured":"A. I. Mal\u2019tsev . 1962 . Axiomatizable classes of locally free algebras of certain types . Sibirsk. Mat. Zh. , 3 (1962), 729 \u2013 743 . A. I. Mal\u2019tsev. 1962. Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. Zh., 3 (1962), 729\u2013743.","journal-title":"Sibirsk. Mat. Zh."},{"key":"e_1_2_1_45_1","volume-title":"Logical Foundations of Computer Science, Sergei N","author":"Manna Zohar","unstructured":"Zohar Manna , Henny B. Sipma , and Ting Zhang . 2007. Verifying Balanced Trees . In Logical Foundations of Computer Science, Sergei N . Artemov and Anil Nerode (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 363\u2013378. isbn:978-3-540-72734-7 Zohar Manna, Henny B. Sipma, and Ting Zhang. 2007. Verifying Balanced Trees. In Logical Foundations of Computer Science, Sergei N. Artemov and Anil Nerode (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 363\u2013378. isbn:978-3-540-72734-7"},{"key":"e_1_2_1_46_1","volume-title":"Hilbert\u2019s Tenth Problem","author":"Matiyasevich Yuri V.","unstructured":"Yuri V. Matiyasevich . 1993. Hilbert\u2019s Tenth Problem . MIT Press , Cambridge, MA, USA . isbn:0262132958 Yuri V. Matiyasevich. 1993. Hilbert\u2019s Tenth Problem. MIT Press, Cambridge, MA, USA. isbn:0262132958"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670416"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563354"},{"key":"e_1_2_1_49_1","volume-title":"Techniques for Program Verification. Ph. D. Dissertation","author":"Nelson Charles Gregory","unstructured":"Charles Gregory Nelson . 1980. Techniques for Program Verification. Ph. D. Dissertation . Stanford University . Stanford, CA, USA. AAI8011683 Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph. D. Dissertation. Stanford University. Stanford, CA, USA. AAI8011683"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_51_1","volume-title":"The Imandra Automated Reasoning System (System Description)","author":"Passmore Grant","unstructured":"Grant Passmore , Simon Cruanes , Denis Ignatovich , Dave Aitken , Matt Bray , Elijah Kagan , Kostya Kanishev , Ewen Maclean , and Nicola Mometto . 2020. The Imandra Automated Reasoning System (System Description) . In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing , Cham . 464\u2013471. isbn:978-3-030-51054-1 Grant Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, and Nicola Mometto. 2020. The Imandra Automated Reasoning System (System Description). In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing, Cham. 464\u2013471. isbn:978-3-030-51054-1"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2494597"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1080\/014453409108837187"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_2_1_56_1","volume-title":"CEUR Workshop Proceedings, 1889 (2017), 1 Jan., 63\u201375. issn:1613-0073 15th International Workshop on Satisfiability Modulo Theories, SMT 2017 ; Conference date: 22-07-2017 Through 23-07-2017","author":"Reger Giles","year":"2017","unstructured":"Giles Reger , Martin Suda , and Andrei Voronkov . 2017 . Instantiation and pretending to be an SMT solver with VAMPIRE . CEUR Workshop Proceedings, 1889 (2017), 1 Jan., 63\u201375. issn:1613-0073 15th International Workshop on Satisfiability Modulo Theories, SMT 2017 ; Conference date: 22-07-2017 Through 23-07-2017 Giles Reger, Martin Suda, and Andrei Voronkov. 2017. Instantiation and pretending to be an SMT solver with VAMPIRE. CEUR Workshop Proceedings, 1889 (2017), 1 Jan., 63\u201375. issn:1613-0073 15th International Workshop on Satisfiability Modulo Theories, SMT 2017 ; Conference date: 22-07-2017 Through 23-07-2017"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.29007\/jmd3"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9372-6"},{"key":"e_1_2_1_59_1","volume-title":"Verification, Model Checking, and Abstract Interpretation, Deepak D\u2019Souza","author":"Reynolds Andrew","unstructured":"Andrew Reynolds and Viktor Kuncak . 2015. Induction for SMT Solvers . In Verification, Model Checking, and Abstract Interpretation, Deepak D\u2019Souza , Akash Lal, and Kim Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg . 80\u201398. isbn:978-3-662-46081-8 Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. In Verification, Model Checking, and Abstract Interpretation, Deepak D\u2019Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 80\u201398. isbn:978-3-662-46081-8"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375602"},{"key":"e_1_2_1_62_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, Nikolaj Bj\u00f8rner and Andrei Voronkov (Eds.)","author":"R\u00fcmmer Philipp","unstructured":"Philipp R\u00fcmmer . 2012. E-Matching with Free Variables . In Logic for Programming, Artificial Intelligence, and Reasoning, Nikolaj Bj\u00f8rner and Andrei Voronkov (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg . 359\u2013374. isbn:978-3-642-28717-6 Philipp R\u00fcmmer. 2012. E-Matching with Free Variables. In Logic for Programming, Artificial Intelligence, and Reasoning, Nikolaj Bj\u00f8rner and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 359\u2013374. isbn:978-3-642-28717-6"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/371316.371494"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563306"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-23-1-150-161"},{"key":"e_1_2_1_66_1","volume-title":"Automated Deduction \u2013 CADE-22, Renate A","author":"Sofronie-Stokkermans Viorica","unstructured":"Viorica Sofronie-Stokkermans . 2009. Locality Results for Certain Extensions of Theories with Bridging Functions . In Automated Deduction \u2013 CADE-22, Renate A . Schmidt (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 67\u201383. isbn:978-3-642-02959-2 Viorica Sofronie-Stokkermans. 2009. Locality Results for Certain Extensions of Theories with Bridging Functions. In Automated Deduction \u2013 CADE-22, Renate A. Schmidt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 67\u201383. isbn:978-3-642-02959-2"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_2_1_68_1","volume-title":"Ali Sinan K\u00f6ksal, and Viktor Kuncak","author":"Suter Philippe","year":"2011","unstructured":"Philippe Suter , Ali Sinan K\u00f6ksal, and Viktor Kuncak . 2011 . Satisfiability Modulo Recursive Programs. In Static Analysis, Eran Yahav (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 298\u2013315. isbn:978-3-642-23702-7 Philippe Suter, Ali Sinan K\u00f6ksal, and Viktor Kuncak. 2011. Satisfiability Modulo Recursive Programs. In Static Analysis, Eran Yahav (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 298\u2013315. isbn:978-3-642-23702-7"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"e_1_2_1_70_1","volume-title":"Zarba","author":"Tinelli Cesare","year":"2004","unstructured":"Cesare Tinelli and Calogero G . Zarba . 2004 . Combining Decision Procedures for Sorted Theories. In Logics in Artificial Intelligence, J\u00f3se J\u00falio Alferes and Jo\u00e3o Leite (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 641\u2013653. isbn:978-3-540-30227-8 Cesare Tinelli and Calogero G. Zarba. 2004. Combining Decision Procedures for Sorted Theories. In Logics in Artificial Intelligence, J\u00f3se J\u00falio Alferes and Jo\u00e3o Leite (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 641\u2013653. isbn:978-3-540-30227-8"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-5204-9"},{"key":"e_1_2_1_72_1","volume-title":"Automating Induction for Solving Horn Clauses","author":"Unno Hiroshi","unstructured":"Hiroshi Unno , Sho Torii , and Hiroki Sakamoto . 2017. Automating Induction for Solving Horn Clauses . In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing , Cham . 571\u2013591. isbn:978-3-319-63390-9 Hiroshi Unno, Sho Torii, and Hiroki Sakamoto. 2017. Automating Induction for Solving Horn Clauses. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 571\u2013591. isbn:978-3-319-63390-9"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"},{"key":"e_1_2_1_75_1","volume-title":"Frontiers of Combining Systems","author":"Wies Thomas","unstructured":"Thomas Wies , Ruzica Piskac , and Viktor Kuncak . 2009. Combining Theories with Shared Set Operations . In Frontiers of Combining Systems , Silvio Ghilardi and Roberto Sebastiani (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 366\u2013382. isbn:978-3-642-04222-5 Thomas Wies, Ruzica Piskac, and Viktor Kuncak. 2009. Combining Theories with Shared Set Operations. In Frontiers of Combining Systems, Silvio Ghilardi and Roberto Sebastiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 366\u2013382. isbn:978-3-642-04222-5"},{"key":"e_1_2_1_76_1","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"Winskel Glynn","unstructured":"Glynn Winskel . 1993. The Formal Semantics of Programming Languages: An Introduction . MIT Press , Cambridge, MA, USA . isbn:0262231697 Glynn Winskel. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, USA. isbn:0262231697"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/321296.321302"},{"key":"e_1_2_1_78_1","volume-title":"Principles and Practice of Constraint Programming, Thomas Schiex and Simon de Givry (Eds.)","author":"Yang Weikun","unstructured":"Weikun Yang , Grigory Fedyukovich , and Aarti Gupta . 2019. Lemma Synthesis for Automating Induction over Algebraic Data Types . In Principles and Practice of Constraint Programming, Thomas Schiex and Simon de Givry (Eds.) . Springer International Publishing , Cham . 600\u2013617. isbn:978-3-030-30048-7 Weikun Yang, Grigory Fedyukovich, and Aarti Gupta. 2019. Lemma Synthesis for Automating Induction over Algebraic Data Types. In Principles and Practice of Constraint Programming, Thomas Schiex and Simon de Givry (Eds.). Springer International Publishing, Cham. 600\u2013617. isbn:978-3-030-30048-7"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.03.004"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622835","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622835","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622835"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":79,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622835"],"URL":"https:\/\/doi.org\/10.1145\/3622835","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}