{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:08Z","timestamp":1772164028729,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,6,16]],"date-time":"2013-06-16T00:00:00Z","timestamp":1371340800000},"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":[[2013,6,16]]},"DOI":"10.1145\/2491956.2462192","type":"proceedings-article","created":{"date-parts":[[2013,6,11]],"date-time":"2013-06-11T12:03:50Z","timestamp":1370952230000},"page":"27-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":96,"title":["Complete completion using types and weights"],"prefix":"10.1145","author":[{"given":"Tihomir","family":"Gvero","sequence":"first","affiliation":[{"name":"Ecole Polytechnique Federale de Lausanne (EPFL), Lausanne, Switzerland"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique Federale de Lausanne (EPFL), Lausanne, Switzerland"}]},{"given":"Ivan","family":"Kuraj","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique Federale de Lausanne (EPFL), Lausanne, Switzerland"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS), Saarbrucken, Germany"}]}],"member":"320","published-online":{"date-parts":[[2013,6,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595728"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_26"},{"key":"e_1_3_2_1_5_1","first-page":"131","volume-title":"TYPES","author":"Delahaye D.","year":"1999","unstructured":"D. Delahaye . Information retrieval in a Coq proof library using type isomorphisms . In TYPES , pages 131 -- 147 , 1999 . D. Delahaye. Information retrieval in a Coq proof library using type isomorphisms. In TYPES, pages 131--147, 1999."},{"key":"e_1_3_2_1_6_1","volume-title":"II: 1009--1062","author":"Dowek G.","year":"2001","unstructured":"G. Dowek . Higher-order unification and matching. Handbook of automated reasoning , II: 1009--1062 , 2001 . G. Dowek. Higher-order unification and matching. Handbook of automated reasoning, II: 1009--1062, 2001."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxn029"},{"key":"e_1_3_2_1_8_1","unstructured":"Eclipse Code Recommenders. http:\/\/www.eclipse.org\/recommenders\/.  Eclipse Code Recommenders. http:\/\/www.eclipse.org\/recommenders\/."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1928380.1928401"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032338"},{"key":"e_1_3_2_1_11_1","volume-title":"EPFL","author":"Gvero T.","year":"2012","unstructured":"T. Gvero , V. Kuncak , I. Kuraj , and R. Piskac . On complete completion using types and weights. Technical report , EPFL , December 2012 . T. Gvero, V. Kuncak, I. Kuraj, and R. Piskac. On complete completion using types and weights. Technical report, EPFL, December 2012."},{"key":"e_1_3_2_1_12_1","unstructured":"Hayoo! API Search. http:\/\/holumbus.fh-wedel.de\/hayoo\/hayoo.html.  Hayoo! API Search. http:\/\/holumbus.fh-wedel.de\/hayoo\/hayoo.html."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062491"},{"key":"e_1_3_2_1_14_1","unstructured":"Hoogle API Search. http:\/\/www.haskell.org\/hoogle\/.  Hoogle API Search. http:\/\/www.haskell.org\/hoogle\/."},{"key":"e_1_3_2_1_15_1","unstructured":"IntelliJ IDEA website 2011. URL http:\/\/www.jetbrains.com\/idea\/.  IntelliJ IDEA website 2011. URL http:\/\/www.jetbrains.com\/idea\/."},{"key":"e_1_3_2_1_16_1","volume-title":"EPFL","author":"Kuraj I.","year":"2013","unstructured":"I. Kuraj . Interactive code generation. Master's thesis , EPFL , February 2013 . I. Kuraj. Interactive code generation. Master's thesis, EPFL, February 2013."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006804"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_19"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254098"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647468.727090"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167508"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90006-9"},{"key":"e_1_3_2_1_25_1","unstructured":"heorem Prover()}DjinnThe Djinn Theorem Prover. http:\/\/www.augustsson.net\/Darcs\/Djinn\/.  heorem Prover()}DjinnThe Djinn Theorem Prover. http:\/\/www.augustsson.net\/Darcs\/Djinn\/."},{"key":"e_1_3_2_1_26_1","unstructured":"The Eclipse Foundation. http:\/\/www.eclipse.org\/.  The Eclipse Foundation. http:\/\/www.eclipse.org\/."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321663"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645893.671612"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11506676_17"}],"event":{"name":"PLDI '13: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Seattle Washington USA","acronym":"PLDI '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2462192","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491956.2462192","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:39:10Z","timestamp":1750221550000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2462192"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,16]]},"references-count":29,"alternative-id":["10.1145\/2491956.2462192","10.1145\/2491956"],"URL":"https:\/\/doi.org\/10.1145\/2491956.2462192","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2499370.2462192","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,6,16]]},"assertion":[{"value":"2013-06-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}