{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:10:57Z","timestamp":1774987857971,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,1,23]],"date-time":"2012-01-23T00:00:00Z","timestamp":1327276800000},"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":[[2012,1,23]]},"DOI":"10.1145\/2103746.2103767","type":"proceedings-article","created":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T16:47:19Z","timestamp":1327423639000},"page":"107-116","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Hybrid contract checking via symbolic simplification"],"prefix":"10.1145","author":[{"given":"Dana N.","family":"Xu","sequence":"first","affiliation":[{"name":"INRIA, Paris-Rocquencourt, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,1,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Combining the Coq proof assistant with first-order decision procedures. Unpublished","author":"Ayache N.","year":"2006","unstructured":"N. Ayache and J.-C. Filliatre . Combining the Coq proof assistant with first-order decision procedures. Unpublished , 2006 . URL http:\/\/www.lri.fr\/ filliatr\/publis\/coq-dp.ps. N. Ayache and J.-C. Filliatre. Combining the Coq proof assistant with first-order decision procedures. Unpublished, 2006. URL http:\/\/www.lri.fr\/ filliatr\/publis\/coq-dp.ps."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987213"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180480"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032277"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005971"},{"key":"e_1_3_2_1_8_1","volume-title":"Ergo : a theorem prover for polymorphic first-order logic modulo theories. Unpublished","author":"Conchon S.","year":"2006","unstructured":"S. Conchon , E. Contejean , and J. Kanig . Ergo : a theorem prover for polymorphic first-order logic modulo theories. Unpublished , 2006 . URL http:\/\/ergo.lri.fr\/papers\/ergo.ps. S. Conchon, E. Contejean, and J. Kanig. Ergo : a theorem prover for polymorphic first-order logic modulo theories. Unpublished, 2006. URL http:\/\/ergo.lri.fr\/papers\/ergo.ps."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_18"},{"key":"e_1_3_2_1_10_1","first-page":"10","volume-title":"FoVeOOS: the Intl. Conf. on Formal Verf. of OO Software","author":"Fahndrich M.","year":"2010","unstructured":"M. Fahndrich and F. Logozzo . Static contract checking with abstract interpretation . In FoVeOOS: the Intl. Conf. on Formal Verf. of OO Software , pages 10 -- 30 , 2010 . M. Fahndrich and F. Logozzo. Static contract checking with abstract interpretation. In FoVeOOS: the Intl. Conf. on Formal Verf. of OO Software, pages 10--30, 2010."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_16"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013963.1013985"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_31"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032343"},{"key":"e_1_3_2_1_22_1","first-page":"137","volume-title":"IJCAI","author":"Kerber M.","year":"1991","unstructured":"M. Kerber . How to prove higher order theorems in first order logic . In IJCAI , pages 137 -- 142 , 1991 . M. Kerber. How to prove higher order theorems in first order logic. In IJCAI, pages 137--142, 1991."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806645"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_29_1","volume-title":"Eiffel: the language","author":"Meyer B.","year":"1992","unstructured":"B. Meyer . Eiffel: the language . Prentice-Hall , 1992 . B. Meyer. Eiffel: the language. Prentice-Hall, 1992."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190247"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926453"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_17"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_19"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159849"},{"key":"e_1_3_2_1_39_1","volume-title":"INRIA technical report RR-7794","author":"Xu D. N.","year":"2011","unstructured":"D. N. Xu . Hybrid contract checking via symbolic simplification. INRIA technical report RR-7794 , 2011 . D. N. Xu. Hybrid contract checking via symbolic simplification. INRIA technical report RR-7794, 2011."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"}],"event":{"name":"POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Philadelphia Pennsylvania USA","acronym":"POPL '12","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103746.2103767","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2103746.2103767","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:35Z","timestamp":1750241195000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103746.2103767"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,23]]},"references-count":40,"alternative-id":["10.1145\/2103746.2103767","10.1145\/2103746"],"URL":"https:\/\/doi.org\/10.1145\/2103746.2103767","relation":{},"subject":[],"published":{"date-parts":[[2012,1,23]]},"assertion":[{"value":"2012-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}