{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:44:02Z","timestamp":1725763442272},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319035444"},{"type":"electronic","value":"9783319035451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03545-1_8","type":"book-chapter","created":{"date-parts":[[2013,12,9]],"date-time":"2013-12-09T16:31:48Z","timestamp":1386606708000},"page":"114-130","source":"Crossref","is-referenced-by-count":6,"title":["Nonfree Datatypes in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Schropp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"The Coq Proof Assistant (2013), http:\/\/coq.inria.fr"},{"key":"8_CR2","unstructured":"Maude ITP (2013), http:\/\/maude.cs.uiuc.edu\/tools\/itp"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-76786-2_4","volume-title":"Datatype-Generic Programming","author":"T. Altenkirch","year":"2007","unstructured":"Altenkirch, T., McBride, C., Morris, P.: Generic programming with dependent types. In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.) SSDGP 2006. LNCS, vol.\u00a04719, pp. 209\u2013257. Springer, Heidelberg (2007)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-71316-6_8","volume-title":"Programming Languages and Systems","author":"F. Blanqui","year":"2007","unstructured":"Blanqui, F., Hardin, T., Weis, P.: On the implementation of construction functions for non-free concrete data types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 95\u2013109. Springer, Heidelberg (2007)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-03153-3_2","volume-title":"Language Engineering and Rigorous Software Development","author":"A. Bove","year":"2009","unstructured":"Bove, A., Dybjer, P.: Dependent types at work. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet ALFA Summer School 2008. LNCS, vol.\u00a05520, pp. 57\u201399. Springer, Heidelberg (2009)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-48685-2_18","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"1999","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: The Maude system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 240\u2013243. Springer, Heidelberg (1999)"},{"key":"8_CR7","unstructured":"CoFI task group on semantics, CASL \u2014 The Common Algebraic Specification Language, Semantics (1999), http:\/\/www.informatik.uni-bremen.de\/cofi\/wiki\/index.php\/CASL"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Coquand, T., Danielsson, N.A.: Isomorphism is equality. Draft (2013)","DOI":"10.1016\/j.indag.2013.09.002"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 160\u2013174. Springer, Heidelberg (2007)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/11541868_9","volume-title":"Theorem Proving in Higher Order Logics","author":"P.V. Homeier","year":"2005","unstructured":"Homeier, P.V.: A design structure for higher order quotients. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 130\u2013146. Springer, Heidelberg (2005)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kuncar, O.: Lifting and transfer: A modular design for quotients in Isabelle\/HOL. In: Isabelle Users Workshop (2012)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-14052-5_5","volume-title":"Interactive Theorem Proving","author":"B. Huffman","year":"2010","unstructured":"Huffman, B., Urban, C.: A new foundation for Nominal Isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 35\u201350. Springer, Heidelberg (2010)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, C.: Quotients revisited for Isabelle\/HOL. In: SAC, pp. 1639\u20131644 (2011)","DOI":"10.1145\/1982185.1982529"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales - A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 149\u2013166. Springer, Heidelberg (1999)"},{"key":"8_CR16","unstructured":"Nadathur, G., Miller, D.: An overview of Lambda-Prolog. In: ICLP\/SLP, pp. 810\u2013827 (1988)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-540-30142-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Norrish","year":"2004","unstructured":"Norrish, M.: Recursive function definition for types with binders. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 241\u2013256. Springer, Heidelberg (2004)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Popescu, A., Gunter, E.L.: Recursion principles for syntax with bindings and substitution. In: ICFP, pp. 346\u2013358 (2011)","DOI":"10.1145\/2034773.2034819"},{"key":"8_CR20","unstructured":"Schropp, A.: Instantiating deeply embedded many-sorted theories into HOL types in Isabelle. Master\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2012), http:\/\/home.in.tum.de\/~schropp\/master-thesis.pdf"},{"key":"8_CR21","unstructured":"Schropp, A., Popescu, A.: Nonfree datatypes: metatheory, implementation and examples, http:\/\/bitbucket.org\/isaspecops\/nonfree-data\/downloads\/cpp2013_bundle.zip"},{"key":"8_CR22","unstructured":"Shulman, M., Licata, D., Lumsdaine, P.L., et al.: Higher inductive types on the homotopy type theory blog, http:\/\/homotopytypetheory.org\/category\/higher-inductive-types\/"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-54233-7_125","volume-title":"Automata, Languages and Programming","author":"V. Breazu-Tannen","year":"1991","unstructured":"Breazu-Tannen, V., Subrahmanyam, R.: Logical and computational aspects of programming with sets\/bags\/lists. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 60\u201375. Springer, Heidelberg (1991)"},{"key":"8_CR24","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 (2012)","DOI":"10.1109\/LICS.2012.75"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03545-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,4]],"date-time":"2019-08-04T18:20:23Z","timestamp":1564942823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03545-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319035444","9783319035451"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03545-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}