{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:04Z","timestamp":1772163964717,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,6,5]],"date-time":"2010-06-05T00:00:00Z","timestamp":1275696000000},"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":[[2010,6,5]]},"DOI":"10.1145\/1806596.1806632","type":"proceedings-article","created":{"date-parts":[[2010,6,8]],"date-time":"2010-06-08T08:37:34Z","timestamp":1275986254000},"page":"316-329","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":84,"title":["Complete functional synthesis"],"prefix":"10.1145","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[{"name":"Swiss Federal Institute of Technology, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mika\u00ebl","family":"Mayer","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,6,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792771"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646875.709990"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/535430"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071596.1071601"},{"key":"e_1_3_2_1_5_1","volume-title":"Bradley and Zohar Manna. The Calculus of Computation","author":"Aaron","year":"2007","unstructured":"Aaron R. Bradley and Zohar Manna. The Calculus of Computation . Springer , 2007 . Aaron R. Bradley and Zohar Manna. The Calculus of Computation. Springer, 2007."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.11.037"},{"key":"e_1_3_2_1_8_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","year":"2001","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Cliff Stein . Introduction to Algorithms ( Second Edition). MIT Press and McGraw-Hill , 2001 . Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliff Stein. Introduction to Algorithms (Second Edition). MIT Press and McGraw-Hill, 2001."},{"key":"e_1_3_2_1_9_1","first-page":"91","volume-title":"Machine Intelligence","author":"Cooper D. C.","year":"1972","unstructured":"D. C. Cooper . Theorem proving in arithmetic without multiplication . In B. Meltzer and D. Michie, editors, Machine Intelligence , volume 7 , pages 91 -- 100 . Edinburgh University Press , 1972 . D. C. Cooper. Theorem proving in arithmetic without multiplication. In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 7, pages 91--100. Edinburgh University Press, 1972."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357064"},{"key":"e_1_3_2_1_11_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra . A Discipline of Programming . Prentice-Hall, Inc. , 1976 . Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Inc., 1976."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2394758.2394779"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.1080.0320"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/648183.749717"},{"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","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"Ferrante Jeanne","year":"1979","unstructured":"Jeanne Ferrante and Charles W. Rackoff . The Computational Complexity of Logical Theories , volume 718 of Lecture Notes in Mathematics . Springer-Verlag , 1979 . Jeanne Ferrante and Charles W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, 1979."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-47-1-57-103"},{"key":"e_1_3_2_1_18_1","first-page":"175","volume-title":"CAV","author":"Ganzinger Harald","year":"2004","unstructured":"Harald Ganzinger , George Hagen , Robert Nieuwenhuis , Albert Oliveras , and Cesare Tinelli . DPLL(T) : Fast decision procedures . In CAV , pages 175 -- 188 , 2004 . Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast decision procedures. In CAV, pages 175--188, 2004."},{"issue":"2","key":"e_1_3_2_1_19_1","first-page":"333","article-title":"Bounded algol-like languages","volume":"113","author":"Ginsburg S.","year":"1964","unstructured":"S. Ginsburg and E. Spanier . Bounded algol-like languages . Transactions of the American Mathematical Society , 113 ( 2 ): 333 -- 368 , 1964 . S. Ginsburg and E. Spanier. Bounded algol-like languages. Transactions of the American Mathematical Society, 113(2):333--368, 1964.","journal-title":"Transactions of the American Mathematical Society"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1966.16.285"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.22"},{"key":"e_1_3_2_1_23_1","volume-title":"Partial Evaluation and Automatic Program Generation. (freely available)","author":"Jones Neil D.","year":"1993","unstructured":"Neil D. Jones , Carsten K. Gomard , and Peter Sestoft . Partial Evaluation and Automatic Program Generation. (freely available) , 1993 . Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. (freely available), 1993."},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","volume-title":"CAV","author":"Jobstmann Barbara","year":"2007","unstructured":"Barbara Jobstmann , Stefan Galler , Martin Weiglhofer , and Roderick Bloem . Anzu: A tool for property synthesis . In CAV , volume 4590 of LNCS , 2007 . Barbara Jobstmann, Stefan Galler, Martin Weiglhofer, and Roderick Bloem. Anzu: A tool for property synthesis. In CAV, volume 4590 of LNCS, 2007."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"e_1_3_2_1_27_1","volume-title":"Department of Computer Science","author":"Klarlund Nils","year":"2001","unstructured":"Nils Klarlund and Anders M\u00f8ller . MONA Version 1.4 User Manual . BRICS Notes Series NS-01-1 , Department of Computer Science , University of Aarhus , January 2001 . Nils Klarlund and Anders M\u00f8ller. MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus, January 2001."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_6"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_15"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158628"},{"key":"e_1_3_2_1_32_1","volume-title":"CAV","author":"James","year":"2000","unstructured":"James H. Kukula and Thomas R. Shiple. Building circuits from relations . In CAV , 2000 . James H. Kukula and Thomas R. Shiple. Building circuits from relations. In CAV, 2000."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_47"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/362566.362568"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_3"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512776"},{"key":"e_1_3_2_1_40_1","volume-title":"Programming in Scala: a comprehensive step-by-step guide","author":"Odersky Martin","year":"2008","unstructured":"Martin Odersky , Lex Spoon , and Bill Venners . Programming in Scala: a comprehensive step-by-step guide . Artima Press , 2008 . Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008."},{"key":"e_1_3_2_1_41_1","series-title":"LNCS","volume-title":"VMCAI","author":"Piskac Ruzica","year":"2008","unstructured":"Ruzica Piskac and Viktor Kuncak . Decision procedures for multisets with cardinality constraints . In VMCAI , volume 4905 of LNCS , 2008 . Ruzica Piskac and Viktor Kuncak. Decision procedures for multisets with cardinality constraints. In VMCAI, volume 4905 of LNCS, 2008."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_25"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_24"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/135226.135233"},{"key":"e_1_3_2_1_47_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","year":"1998","unstructured":"Alexander Schrijver . Theory of Linear and Integer Programming . John Wiley & Sons , 1998 . Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, 1998."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Don Syme Adam Granicz and Antonio Cisternino. Expert F#. Apress 2007.  Don Syme Adam Granicz and Antonio Cisternino. Expert F#. Apress 2007.","DOI":"10.1007\/978-1-4302-0285-1"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357166"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793246252"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250787"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_13"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/258726.258746"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/1807707.1807732"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_27"},{"key":"e_1_3_2_1_61_1","volume-title":"18th International Workshop on Unification","author":"Zarba Calogero G.","year":"2004","unstructured":"Calogero G. Zarba . A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator . In 18th International Workshop on Unification , 2004 . Calogero G. Zarba. A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In 18th International Workshop on Unification, 2004."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-3075-8"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"event":{"name":"PLDI '10: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Toronto Ontario Canada","acronym":"PLDI '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1806596.1806632","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1806596.1806632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:22:31Z","timestamp":1750231351000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1806596.1806632"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6,5]]},"references-count":59,"alternative-id":["10.1145\/1806596.1806632","10.1145\/1806596"],"URL":"https:\/\/doi.org\/10.1145\/1806596.1806632","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1809028.1806632","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,6,5]]},"assertion":[{"value":"2010-06-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}