{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:02Z","timestamp":1780994702420,"version":"3.54.1"},"reference-count":42,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1109\/lics.2017.8005071","type":"proceedings-article","created":{"date-parts":[[2017,8,10]],"date-time":"2017-08-10T20:43:24Z","timestamp":1502397804000},"page":"1-12","source":"Crossref","is-referenced-by-count":8,"title":["Foundational nonuniform (Co)datatypes for higher-order logic"],"prefix":"10.1109","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fabian","family":"Meier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00063-5"},{"key":"ref38","first-page":"513","article-title":"Types, abstraction and parametric polymorphism","author":"reynolds","year":"1983","journal-title":"IFIP '83"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12925-1_41"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900731X"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_47"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_58"},{"key":"ref36","author":"okasaki","year":"1999","journal-title":"Purely Functional Data Structures"},{"key":"ref35","article-title":"Finger trees","author":"nordhoff","year":"2010","journal-title":"Archive of Formal Proofs"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_28"},{"key":"ref10","first-page":"93","article-title":"tel. Truly modular (co) datatypes for Isabelle\/HOL","author":"blanchette","year":"2014","journal-title":"ITP 2014 vol 8558 of LNCS"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291156"},{"key":"ref11","author":"blanchette","year":"2017","journal-title":"tel Formalization and implementation accompanying this paper"},{"key":"ref12","article-title":"Foundational nonuniform (co) datatypes for higher-order logic (report)","author":"blanchette","year":"2017","journal-title":"Tech Report"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784732"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_15"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"ref17","first-page":"173","article-title":"Representing cyclic structures as nested datatypes","author":"ghani","year":"2006","journal-title":"TFP 2006 vol 7 of Trends in Functional Programming"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:12)2012"},{"key":"ref19","author":"gordon","year":"1993","journal-title":"Introduction to HOL A Theorem Proving Environment for Higher Order Logic"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.4153\/CMB-1970-065-6"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.017"},{"key":"ref6","author":"biendarra","year":"2015","journal-title":"Functor-Preserving Type Definitions in Isabelle\/HOL"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0013-6"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_3"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_17"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050047"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_8"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_131"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169692"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60275-5_66"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"ref24","first-page":"1","article-title":"Efficient generalized folds","author":"hinze","year":"2000","journal-title":"Workshop on Generic Programming"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.75"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9207-9"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005769"}],"event":{"name":"2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","location":"Reykjavik, Iceland","start":{"date-parts":[[2017,6,20]]},"end":{"date-parts":[[2017,6,23]]}},"container-title":["2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7999337\/8005055\/08005071.pdf?arnumber=8005071","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,30]],"date-time":"2017-08-30T04:24:22Z","timestamp":1504067062000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8005071\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6]]},"references-count":42,"URL":"https:\/\/doi.org\/10.1109\/lics.2017.8005071","relation":{},"subject":[],"published":{"date-parts":[[2017,6]]}}}