{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T12:08:40Z","timestamp":1763726920647,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,6,13]],"date-time":"2015-06-13T00:00:00Z","timestamp":1434153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["IMPRO"],"award-info":[{"award-number":["IMPRO"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001711","name":"Schweizerische Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["200021_144503"],"award-info":[{"award-number":["200021_144503"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,6,13]]},"DOI":"10.1145\/2774975.2774978","type":"proceedings-article","created":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T15:35:56Z","timestamp":1433345756000},"page":"18-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Counter-example complete verification for higher-order functions"],"prefix":"10.1145","author":[{"given":"Nicolas","family":"Voirol","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}]},{"given":"Etienne","family":"Kneuss","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2015,6,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_1_2_1","series-title":"EPiC Series","first-page":"10","volume-title":"PxTP","author":"Benzm\u00fcller C.","year":"2013","unstructured":"C. Benzm\u00fcller and N. Sultana . LEO-II version 1.5 . In PxTP 2013 , volume 14 of EPiC Series , pages 2\u2013 10 , 2013. C. Benzm\u00fcller and N. Sultana. LEO-II version 1.5. In PxTP 2013, volume 14 of EPiC Series, pages 2\u201310, 2013."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"e_1_3_2_1_5_1","volume-title":"Interactive theorem proving and program development. Coq\u2019Art","author":"Cast\u00e9ran P.","year":"2004","unstructured":"P. Cast\u00e9ran and Y. Bertot . Interactive theorem proving and program development. Coq\u2019Art . Springer Verlag , 2004 . P. Cast\u00e9ran and Y. Bertot. Interactive theorem proving and program development. Coq\u2019Art. Springer Verlag, 2004."},{"key":"e_1_3_2_1_6_1","volume-title":"Computer-aided reasoning: an approach","author":"Kaufmann M.","year":"2000","unstructured":"M. Kaufmann , J. S. Moore , and P. Manolios . Computer-aided reasoning: an approach . Kluwer Academic Publishers , 2000 . M. Kaufmann, J. S. Moore, and P. Manolios. Computer-aided reasoning: an approach. Kluwer Academic Publishers, 2000."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706355"},{"key":"e_1_3_2_1_9_1","volume-title":"MIT-CSAIL-TR-2014-018","author":"Milicevic A.","year":"2014","unstructured":"A. Milicevic , J. P. Near , E. Kang , and D. Jackson . Alloy*: A Higher-Order Relational Constraint Solver. Technical report , MIT-CSAIL-TR-2014-018 , 2014 . URL http: \/\/hdl.handle.net\/1721.1\/89157. A. Milicevic, J. P. Near, E. Kang, and D. Jackson. Alloy*: A Higher-Order Relational Constraint Solver. Technical report, MIT-CSAIL-TR-2014-018, 2014. URL http: \/\/hdl.handle.net\/1721.1\/89157."},{"key":"e_1_3_2_1_10_1","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL - A Proof Assistant for Higher-Order Logic . Springer , 2002 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939399.1939405"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926453"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54007"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041575"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"}],"event":{"name":"PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Portland OR USA","acronym":"PLDI '15"},"container-title":["Proceedings of the 6th ACM SIGPLAN Symposium on Scala"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2774975.2774978","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2774975.2774978","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:56:05Z","timestamp":1750272965000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2774975.2774978"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,13]]},"references-count":18,"alternative-id":["10.1145\/2774975.2774978","10.1145\/2774975"],"URL":"https:\/\/doi.org\/10.1145\/2774975.2774978","relation":{},"subject":[],"published":{"date-parts":[[2015,6,13]]},"assertion":[{"value":"2015-06-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}