{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:49Z","timestamp":1774837969815,"version":"3.50.1"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661667","type":"print"},{"value":"9783319661674","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_1","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T07:15:18Z","timestamp":1503904518000},"page":"3-21","source":"Crossref","is-referenced-by-count":7,"title":["Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic"],"prefix":"10.1007","author":[{"given":"Julian","family":"Biendarra","sequence":"first","affiliation":[]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[]},{"given":"Aymeric","family":"Bouzy","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Desharnais","sequence":"additional","affiliation":[]},{"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[]},{"given":"Johannes","family":"H\u00f6lzl","sequence":"additional","affiliation":[]},{"given":"Ond\u0159ej","family":"Kun\u010dar","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Lochbihler","sequence":"additional","affiliation":[]},{"given":"Fabian","family":"Meier","sequence":"additional","affiliation":[]},{"given":"Lorenz","family":"Panny","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Sternagel","sequence":"additional","affiliation":[]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[]},{"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"issue":"2","key":"1_CR1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1017\/S0960129502003900","volume":"13","author":"F Bartels","year":"2003","unstructured":"Bartels, F.: Generalised coinduction. Math. Struct. Comput. Sci. 13(2), 321\u2013348 (2003)","journal-title":"Math. Struct. Comput. Sci."},{"key":"1_CR2","unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of Knuth\u2013Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). Formal proof development. http:\/\/isa-afp.org\/entries\/Lambda_Free_KBOs.shtml"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-319-63046-5_27","volume-title":"Automated Deduction \u2013 CADE-26","author":"H Becker","year":"2017","unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: A transfinite Knuth\u2013Bendix order for lambda-free higher-order terms. In: de Moura, L. (ed.) CADE-26. LNCS, vol. 10395, pp. 432\u2013453. Springer, Cham (2017). doi: 10.1007\/978-3-319-63046-5_27"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S Berghofer","year":"1999","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL\u2014lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 19\u201336. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48256-3_3"},{"key":"1_CR5","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2013Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development\u2013Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004). doi: 10.1007\/978-3-662-07964-5"},{"issue":"1","key":"1_CR6","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/s11219-011-9148-5","volume":"21","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C.: Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions. Softw. Qual. J. 21(1), 101\u2013126 (2013)","journal-title":"Softw. Qual. J."},{"key":"1_CR7","unstructured":"Blanchette, J.C., Fleury, M., Traytel, D.: Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle\/HOL. In: Miller, D. (ed.) FSCD 2017. LIPIcs, vol. 84, pp. 11:1\u201311:17 (2017). Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14052-5_11"},{"issue":"1","key":"1_CR9","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/s10817-016-9391-3","volume":"58","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149\u2013179 (2017)","journal-title":"J. Autom. Reason."},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-662-54434-1_5","volume-title":"Programming Languages and Systems","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Bouzy, A., Lochbihler, A., Popescu, A., Traytel, D.: Friends with benefits. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 111\u2013140. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54434-1_5"},{"key":"1_CR11","unstructured":"Blanchette, J.C., Fleury, M., Traytel, D.: Formalization of nested multisets, hereditary multisets, and syntactic ordinals. Archive of Formal Proofs (2016). Formal proof development. http:\/\/isa-afp.org\/entries\/Nested_Multisets_Ordinals.shtml"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Cham (2014). doi: 10.1007\/978-3-319-08970-6_7"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: Ouaknine, J. (ed.) LICS 2017. IEEE Computer Society (2017)","DOI":"10.1109\/LICS.2017.8005071"},{"key":"1_CR14","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Abstract completeness. Archive of Formal Proofs (2014). Formal proof development. http:\/\/isa-afp.org\/entries\/Abstract_Completeness.shtml"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-08970-6_8","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 111\u2013127. Springer, Cham (2014). doi: 10.1007\/978-3-319-08970-6_8"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-319-08587-6_4","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 46\u201360. Springer, Cham (2014). doi: 10.1007\/978-3-319-08587-6_4"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion\u2013a proof assistant perspective. In: Fisher, K., Reppy, J.H. (eds.) ICFP 2015, pp. 192\u2013204. ACM (2015)","DOI":"10.1145\/2784731.2784732"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-662-46669-8_15","volume-title":"Programming Languages and Systems","author":"JC Blanchette","year":"2015","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Witnessing (co)datatypes. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 359\u2013382. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46669-8_15"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-540-74591-4_5","volume-title":"Theorem Proving in Higher Order Logics","author":"L Bulwahn","year":"2007","unstructured":"Bulwahn, L., Krauss, A., Nipkow, T.: Finding lexicographic orders for termination proofs in Isabelle\/HOL. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 38\u201353. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74591-4_5"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-09510-1_15","volume-title":"Automata, Languages and Programming","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. In: Maurer, H.A. (ed.) ICALP 1979. LNCS, vol. 71, pp. 188\u2013202. Springer, Heidelberg (1979). doi: 10.1007\/3-540-09510-1_15"},{"key":"1_CR21","unstructured":"G\u00f6del, K.: \u00dcber die Vollst\u00e4ndigkeit des Logikkalk\u00fcls. Ph.D. thesis, Universit\u00e4t Wien (1929)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Gunter, E.L.: Why we can\u2019t have SML-style datatype declarations in HOL. In: TPHOLs 1992. IFIP Transactions, vol. A-20, pp. 561\u2013568. North-Holland\/Elsevier (1993)","DOI":"10.1016\/B978-0-444-89880-7.50042-5"},{"issue":"2","key":"1_CR23","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1017\/S0956796805005769","volume":"16","author":"R Hinze","year":"2006","unstructured":"Hinze, R., Paterson, R.: Finger trees: a simple general-purpose data structure. J. Funct. Program. 16(2), 197\u2013217 (2006)","journal-title":"J. Funct. Program."},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"H\u00f6lzl, J.: Markov chains and Markov decision processes in Isabelle\/HOL. J. Autom. Reason. doi: 10.1007\/s10817-016-9401-5","DOI":"10.1007\/s10817-016-9401-5"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J.: Markov processes in Isabelle\/HOL. In: Bertot, Y., Vafeiadis, V. (eds.) CPP 2017, pp. 100\u2013111. ACM (2017)","DOI":"10.1145\/3018610.3018628"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Cham (2013). doi: 10.1007\/978-3-319-03545-1_9"},{"key":"1_CR27","volume-title":"Mathematical Logic","author":"SC Kleene","year":"1967","unstructured":"Kleene, S.C.: Mathematical Logic. Wiley, New York (1967)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, pp. 260\u2013270. ACM (2017)","DOI":"10.1145\/3009837.3009887"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 589\u2013603. Springer, Heidelberg (2006). doi: 10.1007\/11814771_48"},{"key":"1_CR30","unstructured":"Lochbihler, A.: Jinja with threads. Archive of Formal Proofs (2007). Formal proof development. http:\/\/isa-afp.org\/entries\/JinjaThreads.shtml"},{"key":"1_CR31","unstructured":"Lochbihler, A.: Coinductive. Archive of Formal Proofs (2010). Formal proof development. http:\/\/afp.sf.net\/entries\/Coinductive.shtml"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-11957-6_23","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2010","unstructured":"Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427\u2013447. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11957-6_23"},{"issue":"4","key":"1_CR33","first-page":"12:1","volume":"35","author":"A Lochbihler","year":"2014","unstructured":"Lochbihler, A.: Making the Java memory model safe. ACM Trans. Program. Lang. Syst. 35(4), 12:1\u201312:65 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-662-49498-1_20","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2016","unstructured":"Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503\u2013531. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49498-1_20"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-319-08970-6_22","volume-title":"Interactive Theorem Proving","author":"A Lochbihler","year":"2014","unstructured":"Lochbihler, A., H\u00f6lzl, J.: Recursive functions on lazy lists via domains and topologies. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 341\u2013357. Springer, Cham (2014). doi: 10.1007\/978-3-319-08970-6_22"},{"key":"1_CR36","unstructured":"Meier, F.: Non-uniform datatypes in Isabelle\/HOL. M.Sc. thesis, ETH Z\u00fcrich (2016)"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Milius, S., Moss, L.S., Schwencke, D.: Abstract GSOS rules and a modular treatment of recursive definitions. Log. Methods Comput. Sci. 9(3), 1\u201352 (2013)","DOI":"10.2168\/LMCS-9(3:28)2013"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45949-9"},{"key":"1_CR40","volume-title":"Purely Functional Data Structures","author":"C Okasaki","year":"1999","unstructured":"Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1999)"},{"key":"1_CR41","unstructured":"Panny, L.: Primitively (co)recursive function definitions for Isabelle\/HOL. B.Sc. thesis, Technische Universit\u00e4t M\u00fcnchen (2014)"},{"issue":"3","key":"1_CR42","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s10817-016-9372-6","volume":"58","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reason. 58(3), 341\u2013362 (2017)","journal-title":"J. Autom. Reason."},{"key":"1_CR43","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP 1983, pp. 513\u2013523 (1983)"},{"key":"1_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/BFb0055624","volume-title":"CONCUR\u201998 Concurrency Theory","author":"JJMM Rutten","year":"1998","unstructured":"Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 194\u2013218. Springer, Heidelberg (1998). doi: 10.1007\/BFb0055624"},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-03545-1_8","volume-title":"Certified Programs and Proofs","author":"A Schropp","year":"2013","unstructured":"Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 114\u2013130. Springer, Cham (2013). doi: 10.1007\/978-3-319-03545-1_8"},{"key":"1_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-319-22102-1_28","volume-title":"Interactive Theorem Proving","author":"C Sternagel","year":"2015","unstructured":"Sternagel, C., Thiemann, R.: Deriving comparators and show functions in Isabelle\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 421\u2013437. Springer, Cham (2015). doi: 10.1007\/978-3-319-22102-1_28"},{"key":"1_CR47","unstructured":"Sternagel, C., Thiemann, R.: Deriving class instances for datatypes. Archive of Formal Proofs (2015). Formal proof development. http:\/\/isa-afp.org\/entries\/Deriving.shtml"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452\u2013468. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03359-9_31"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-71209-1_49"},{"key":"1_CR50","unstructured":"Traytel, D.: Formal languages, formally and coinductively. In: Kesner, D., Pientka, B. (eds.) FSCD 2016. LIPIcs, vol. 52, pp. 31:1\u201331:17 (2016). Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic\u2014category theory applied to theorem proving. In: LICS 2012, pp. 596\u2013605. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.75"},{"key":"1_CR52","unstructured":"Traytel, D.: A category theory based (co)datatype package for Isabelle\/HOL. M.Sc. thesis, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"issue":"23","key":"1_CR53","first-page":"277","volume":"10","author":"M Wenzel","year":"2007","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a generic framework for human-readable proof documents. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric 10(23), 277\u2013298 (2007). Uniwersytet w Bia\u0142ymstoku","journal-title":"From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric"},{"key":"1_CR54","unstructured":"Wenzel, M.: Re: [isabelle] \u201cUnfolding\u201d the sum-of-products encoding of datatypes (2015). https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2015-November\/msg00082.html"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66167-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T17:14:15Z","timestamp":1570036455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}