{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T08:11:55Z","timestamp":1785399115575,"version":"3.56.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,21]],"date-time":"2009-01-21T00:00:00Z","timestamp":1232496000000},"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":[[2009,1,21]]},"DOI":"10.1145\/1480881.1480915","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T09:41:38Z","timestamp":1232444498000},"page":"264-276","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":135,"title":["Equality saturation"],"prefix":"10.1145","author":[{"given":"Ross","family":"Tate","sequence":"first","affiliation":[{"name":"University of Califorina, San Diego, San Diego, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Stepp","sequence":"additional","affiliation":[{"name":"University of Califorina, San Diego, San Diego, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Califorina, San Diego, San Diego, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sorin","family":"Lerner","sequence":"additional","affiliation":[{"name":"University of Califorina, San Diego, San Diego, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,1,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/997163.997196"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359715"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_3_2_1_5_1","volume-title":"Introduction to Functional Programming","author":"Bird R.","year":"1988","unstructured":"R. Bird and P. Wadler . Introduction to Functional Programming . Prentice Hall , 1988 . R. Bird and P. Wadler. Introduction to Functional Programming. Prentice Hall, 1988."},{"key":"e_1_3_2_1_6_1","first-page":"353","volume-title":"The TAMPR program transformation system: simplifying the development of numerical software. Modern software tools for scientific computing","author":"Boyle James M.","year":"1997","unstructured":"James M. Boyle , Terence J. Harmer , and Victor L. Winter . The TAMPR program transformation system: simplifying the development of numerical software. Modern software tools for scientific computing , pages 353 -- 372 , 1997 . James M. Boyle, Terence J. Harmer, and Victor L. Winter. The TAMPR program transformation system: simplifying the development of numerical software. Modern software tools for scientific computing, pages 353--372, 1997."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.11.003"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/201059.201061"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207154"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/314403.314414"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75280"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/182409.182489"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_14_1","first-page":"27","volume-title":"Go to statement considered harmful","author":"Dijkstra E.","year":"1979","unstructured":"E. Dijkstra . Go to statement considered harmful . pages 27 -- 33 , 1979 . E. Dijkstra. Go to statement considered harmful. pages 27--33, 1979."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/131080.131089"},{"key":"e_1_3_2_1_17_1","volume-title":"Expert Systems -- Principles and Programming","author":"Giarratano J.","year":"1993","unstructured":"J. Giarratano and G. Riley . Expert Systems -- Principles and Programming . PWS Publishing Company , 1993 . J. Giarratano and G. Riley. Expert Systems -- Principles and Programming. PWS Publishing Company, 1993."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143146"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/645671.665393"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013208.1013209"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015729001611"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503298"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36194"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93578"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99595"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691453"},{"key":"e_1_3_2_1_31_1","first-page":"61","article-title":"Pueblo: A hybrid pseudo-boolean SAT solver. Journal on Satisfiability","volume":"2","author":"Sheini H.","year":"2006","unstructured":"H. Sheini and K. Sakallah . Pueblo: A hybrid pseudo-boolean SAT solver. Journal on Satisfiability , Boolean Modeling and Computation , 2 : 61 -- 96 , 2006 . H. Sheini and K. Sakallah. Pueblo: A hybrid pseudo-boolean SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 2:61--96, 2006.","journal-title":"Boolean Modeling and Computation"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/645388.651584"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207115"},{"key":"e_1_3_2_1_35_1","volume-title":"CASCON","author":"Vallee-Rai R.","year":"1999","unstructured":"R. Vallee-Rai , L. Hendren , V. Sundaresan , P. Lam , E. Gagnon , and P. Co . Soot -- a Java optimization framework . In CASCON , 1999 . R. Vallee-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot -- a Java optimization framework. In CASCON, 1999."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/567097.567099"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289425"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177907"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/99163.99179"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.267960"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375611"},{"issue":"3","key":"e_1_3_2_1_42_1","first-page":"223","article-title":"A methodology for the translation validation of optimizing compilers","volume":"9","author":"Zuck Lenore","year":"2003","unstructured":"Lenore Zuck , Amir Pnueli , Yi Fang , and Benjamin Goldberg . VOC : A methodology for the translation validation of optimizing compilers . Journal of Universal Computer Science , 9 ( 3 ): 223 -- 247 , March 2003 . Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science, 9(3):223--247, March 2003.","journal-title":"Journal of Universal Computer Science"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Savannah GA USA","acronym":"POPL09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480915","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1480881.1480915","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:29:59Z","timestamp":1750238999000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480915"}},"subtitle":["a new approach to optimization"],"short-title":[],"issued":{"date-parts":[[2009,1,21]]},"references-count":41,"alternative-id":["10.1145\/1480881.1480915","10.1145\/1480881"],"URL":"https:\/\/doi.org\/10.1145\/1480881.1480915","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1594834.1480915","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,1,21]]},"assertion":[{"value":"2009-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}