{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:45:39Z","timestamp":1772163939150,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":67,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,17]],"date-time":"2010-01-17T00:00:00Z","timestamp":1263686400000},"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,1,17]]},"DOI":"10.1145\/1706299.1706325","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T15:15:04Z","timestamp":1263914104000},"page":"199-210","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":57,"title":["Decision procedures for algebraic data types with abstractions"],"prefix":"10.1145","author":[{"given":"Philippe","family":"Suter","sequence":"first","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mirco","family":"Dotta","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique F\u00e9d\u00e9rale de Lausanne, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,1,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_21"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_4_1","unstructured":"C. Barrett S. Ranise A. Stump and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/www.SMT-LIB.org 2009.  C. Barrett S. Ranise A. Stump and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/www.SMT-LIB.org 2009."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.11.037"},{"key":"e_1_3_2_1_6_1","volume-title":"CAV","author":"Barrett C.","year":"2007","unstructured":"C. Barrett and C. Tinelli . CVC3 . In CAV , 2007 . C. Barrett and C. Tinelli. CVC3. In CAV, 2007."},{"key":"e_1_3_2_1_7_1","volume-title":"Verification of Object-Oriented Software: The KeY Approach. LNCS 4334","author":"Beckert B.","year":"2007","unstructured":"B. Beckert , R. H\u00e4hnle , and P.H. Schmitt , editors . Verification of Object-Oriented Software: The KeY Approach. LNCS 4334 . Springer , 2007 . B. Beckert, R. H\u00e4hnle, and P.H. Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer, 2007."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_3_2_1_11_1","volume-title":"The Calculus of Computation","author":"Bradley A.R.","year":"2007","unstructured":"A.R. Bradley and Z. Manna . The Calculus of Computation . Springer , 2007 . A.R. Bradley and Z. Manna. The Calculus of Computation. Springer, 2007."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113469"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1056"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964025"},{"key":"e_1_3_2_1_20_1","volume-title":"VERIFY","author":"Fontaine P.","year":"2007","unstructured":"P. Fontaine . Combinations of theories and the Bernays-Sch\u00f6nfinkel-Ramsey class . In VERIFY , 2007 . P. Fontaine. Combinations of theories and the Bernays-Sch\u00f6nfinkel-Ramsey class. In VERIFY, 2007."},{"key":"e_1_3_2_1_21_1","volume-title":"CAV","author":"Ganzinger H.","year":"2004","unstructured":"H. Ganzinger , G. Hagen , R. Nieuwenhuis , A. Oliveras , and C. Tinelli . DPLL(T): Fast decision procedures . In CAV , 2004 . H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In CAV, 2004."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_3_2_1_25_1","series-title":"Encyclopedia of Mathematics and its Applications","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"Hodges W.","year":"1993","unstructured":"W. Hodges . Model Theory , volume 42 of Encyclopedia of Mathematics and its Applications . Cambridge University Press , 1993 . W. Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)90008-6"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792759"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/78935.78938"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763569"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.125"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789075"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.022"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_15"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111048"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_21"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"e_1_3_2_1_42_1","volume-title":"The Metamathematics of Algebraic Systems","volume":"66","author":"Mal'cev A.I.","year":"1971","unstructured":"A.I. Mal'cev . Chapter 23 : Axiomatizable classes of locally free algebras of various types . In The Metamathematics of Algebraic Systems , volume 66 . North Holland , 1971 . A.I. Mal'cev. Chapter 23: Axiomatizable classes of locally free algebras of various types. In The Metamathematics of Algebraic Systems, volume 66. North Holland, 1971."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72734-7_26"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/367177.367199"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_47"},{"key":"e_1_3_2_1_46_1","series-title":"LNCS","volume-title":"FPCA","author":"Meijer E.","year":"1991","unstructured":"E. Meijer , M. Fokkinga , and R. Paterson . Functional programming with bananas, lenses, envelopes and barbed wire . In FPCA , volume 523 of LNCS , 1991 . E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA, volume 523 of LNCS, 1991."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763074"},{"key":"e_1_3_2_1_51_1","volume-title":"Programming in Scala: a comprehensive step-by-step guide","author":"Odersky M.","year":"2008","unstructured":"M. Odersky , L. Spoon , and B. Venners . Programming in Scala: a comprehensive step-by-step guide . Artima Press , 2008 . M. Odersky, L. Spoon, and B. Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511530104","volume-title":"Purely Functional Data Structures","author":"Okasaki C.","year":"1998","unstructured":"C. Okasaki . Purely Functional Data Structures . Cambridge University Press , 1998 . C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512776"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322287"},{"key":"e_1_3_2_1_55_1","volume-title":"VMCAI, number 4905 in LNCS","author":"Piskac R.","year":"2008","unstructured":"R. Piskac and V. Kuncak . Decision procedures for multisets with cardinality constraints . In VMCAI, number 4905 in LNCS , 2008 . R. Piskac and V. Kuncak. Decision procedures for multisets with cardinality constraints. In VMCAI, number 4905 in LNCS, 2008."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_25"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/990308.990312"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/371316.371494"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_5"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-5204-9"},{"key":"e_1_3_2_1_63_1","volume-title":"Workshop on Types in Compilation","author":"Walker D.","year":"2000","unstructured":"D. Walker and G. Morrisett . Alias types for recursive data structures . In Workshop on Types in Compilation , 2000 . D. Walker and G. Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation, 2000."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_11"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/1807707.1807732"},{"issue":"8","key":"e_1_3_2_1_66_1","first-page":"851","article-title":"Dependently typed pattern matching","volume":"9","author":"Xi H.","year":"2003","unstructured":"H. Xi . Dependently typed pattern matching . Journal of Universal Computer Science , 9 ( 8 ): 851 -- 872 , 2003 . H. Xi. Dependently typed pattern matching. Journal of Universal Computer Science, 9(8):851--872, 2003.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_10"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.004"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"event":{"name":"POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Madrid Spain","acronym":"POPL '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706325","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1706299.1706325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:26:19Z","timestamp":1750263979000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,17]]},"references-count":67,"alternative-id":["10.1145\/1706299.1706325","10.1145\/1706299"],"URL":"https:\/\/doi.org\/10.1145\/1706299.1706325","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1707801.1706325","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,1,17]]},"assertion":[{"value":"2010-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}