{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:20Z","timestamp":1780994780320,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,6,10]],"date-time":"2007-06-10T00:00:00Z","timestamp":1181433600000},"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":[[2007,6,10]]},"DOI":"10.1145\/1250734.1250750","type":"proceedings-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T12:07:37Z","timestamp":1189771657000},"page":"135-145","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Automatic inference of optimizer flow functions from semantic meanings"],"prefix":"10.1145","author":[{"given":"Erika Rice","family":"Scherpelz","sequence":"first","affiliation":[{"name":"Google, Kirkland, WA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sorin","family":"Lerner","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Craig","family":"Chambers","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, WA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2007,6,10]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_4_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable R. L.","year":"1986","unstructured":"R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , and S. F. Smith . Implementing Mathematics with the Nuprl Proof Development System . Prentice-Hall , 1986 . R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"e_1_3_2_1_5_1","series-title":"LNCS","volume-title":"Verification Theory & Practice","author":"Cousot Patrick","year":"2003","unstructured":"Patrick Cousot . Verification by abstract interpretation . In Verification Theory & Practice , volume 2772 of LNCS . Springer-Verlag , 2003 . Patrick Cousot. Verification by abstract interpretation. In Verification Theory & Practice, volume 2772 of LNCS. Springer-Verlag, 2003."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733798"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/535661"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_12_1","volume-title":"The Boyer-Moore theorem prover and its interactive enhancement. Computers and Mathematics with Applications, 29(2)","author":"Kauffmann M.","year":"1995","unstructured":"M. Kauffmann and R. S. Boyer . The Boyer-Moore theorem prover and its interactive enhancement. Computers and Mathematics with Applications, 29(2) , 1995 . M. Kauffmann and R. S. Boyer. The Boyer-Moore theorem prover and its interactive enhancement. Computers and Mathematics with Applications, 29(2), 1995."},{"key":"e_1_3_2_1_13_1","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann M.","year":"2000","unstructured":"M. Kaufmann , P. Manolios , and J. S. Moore . Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers , 2000 . M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_5"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781156"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040335"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647169.718161"},{"key":"e_1_3_2_1_19_1","series-title":"LNAI","volume-title":"Automated Deduction (CADE)","author":"Owre S.","year":"1992","unstructured":"S. Owre , J.M. Rushby , and N. Shankar . PVS: A prototype verification system . In Automated Deduction (CADE) , volume 607 of LNAI . Springer-Verlag , 1992 . S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. In Automated Deduction (CADE), volume 607 of LNAI. Springer-Verlag, 1992."},{"key":"e_1_3_2_1_20_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"Paulson L. C.","year":"1994","unstructured":"L. C. Paulson . Isabelle: A generic theorem prover , volume 828 of LNCS . Springer-Verlag , 1994 . L. C. Paulson. Isabelle: A generic theorem prover, volume 828 of LNCS. Springer-Verlag, 1994."},{"key":"e_1_3_2_1_21_1","series-title":"LNAI","volume-title":"Automated Deduction (CADE)","author":"Pfenning F.","year":"1999","unstructured":"F. Pfenning and C. Schurmann . Sytsem description: Twelf -- a metalogical framework for deductive systems . In Automated Deduction (CADE) , volume 1632 of LNAI . Springer-Verlag , July 1999 . F. Pfenning and C. Schurmann. Sytsem description: Twelf -- a metalogical framework for deductive systems. In Automated Deduction (CADE), volume 1632 of LNAI. Springer-Verlag, July 1999."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134650.1134657"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024410"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36575-3_26"},{"key":"e_1_3_2_1_25_1","volume-title":"Verification, Model Checking","author":"Reps Thomas","year":"2004","unstructured":"Thomas Reps , Mooly Sagiv , and Greta Yorsh . Symbolic implementation of the best transformer . In Verification, Model Checking , and Abstract Interpretation (VMCAI) , January 2004 . Thomas Reps, Mooly Sagiv, and Greta Yorsh. Symbolic implementation of the best transformer. In Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2004."},{"key":"e_1_3_2_1_26_1","volume-title":"Workshop on Compiler Optimization Meets Compiler Verification (COCV)","author":"Rice Erika","year":"2005","unstructured":"Erika Rice , Sorin Lerner , and Craig Chambers . Automatically inferring sound dataflow functions from dataflow fact schemas . In Workshop on Compiler Optimization Meets Compiler Verification (COCV) , April 2005 . Erika Rice, Sorin Lerner, and Craig Chambers. Automatically inferring sound dataflow functions from dataflow fact schemas. In Workshop on Compiler Optimization Meets Compiler Verification (COCV), April 2005."},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","volume-title":"Automated Deduction (CADE)","author":"Schurmann C.","year":"1998","unstructured":"C. Schurmann and F. Pfenning . Automated theorem proving in a simple metalogic for LF . In Automated Deduction (CADE) , volume 1421 of LNCS . Springer-Verlag , July 1998 . C. Schurmann and F. Pfenning. Automated theorem proving in a simple metalogic for LF. In Automated Deduction (CADE), volume 1421 of LNCS. Springer-Verlag, July 1998."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_39"}],"event":{"name":"PLDI '07: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"San Diego California USA","acronym":"PLDI '07","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1250734.1250750","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1250734.1250750","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:19Z","timestamp":1750243939000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1250734.1250750"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,10]]},"references-count":26,"alternative-id":["10.1145\/1250734.1250750","10.1145\/1250734"],"URL":"https:\/\/doi.org\/10.1145\/1250734.1250750","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1273442.1250750","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2007,6,10]]},"assertion":[{"value":"2007-06-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}