{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:39:45Z","timestamp":1767926385892,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_24","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"339-354","source":"Crossref","is-referenced-by-count":34,"title":["The Isabelle Collections Framework"],"prefix":"10.1007","author":[{"given":"Peter","family":"Lammich","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Lochbihler","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11812289_4","volume-title":"Mathematical Knowledge Management","author":"C. Ballarin","year":"2006","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: Theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 31\u201343. Springer, Heidelberg (2006)"},{"key":"24_CR2","first-page":"147","volume-title":"TPHOLs \u201909","author":"S. Berghofer","year":"2009","unstructured":"Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: TPHOLs \u201909, pp. 147\u2013163. Springer, Heidelberg (2009)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 134\u2013149. Springer, Heidelberg (2008)"},{"key":"24_CR4","unstructured":"The Coq standard library, \n                    \n                      http:\/\/coq.inria.fr\/stdlib\/index.html"},{"key":"24_CR5","first-page":"196","volume-title":"TPHOLs \u201909","author":"J. Dios de","year":"2009","unstructured":"de Dios, J., Pe\u00f1a, R.: Formal certification of a resource-aware language implementation. In: TPHOLs \u201909, pp. 196\u2013211. Springer, Heidelberg (2009)"},{"key":"24_CR6","unstructured":"Genet, T., Tong, V.V.T.: Timbuk 2.2., \n                    \n                      http:\/\/www.irisa.fr\/celtique\/genet\/timbuk\/"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Functional and Logic Programming (FLOPS 2010)","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Functional and Logic Programming (FLOPS 2010). LNCS. Springer, Heidelberg (2010)"},{"key":"24_CR8","first-page":"76","volume":"48","author":"G.H. Hardy","year":"1917","unstructured":"Hardy, G.H., Ramanujan, S.: The normal number of prime factors of a number. Quart. J. of Math.\u00a048, 76\u201392 (1917)","journal-title":"Quart. J. of Math."},{"key":"24_CR9","unstructured":"Java: The collections framework, \n                    \n                      http:\/\/java.sun.com\/javase\/6\/docs\/technotes\/guides\/collections\/"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common lisp. IEEE Transactions on Software Engineering\u00a023, 203\u2013213 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR11","unstructured":"Kuncak, V.: Binary search trees. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs. Formal proof development (2004), \n                    \n                      http:\/\/afp.sf.net\/entries\/BinarySearchTree.shtml"},{"key":"24_CR12","unstructured":"Lammich, P.: Isabelle collection library. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs. Formal proof development (2009), \n                    \n                      http:\/\/afp.sf.net\/entries\/collections.shtml"},{"key":"24_CR13","unstructured":"Lammich, P.: Tree automata. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs. Formal proof development (2009), \n                    \n                      http:\/\/afp.sf.net\/entries\/Tree-Automata.shtml"},{"key":"24_CR14","unstructured":"LETHAL tree and hedge automata library, \n                    \n                      http:\/\/lethal.sourceforge.net\/"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"24_CR16","unstructured":"Nipkow, T., Pusch, C.: AVL trees. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs. Formal proof development (2004), \n                    \n                      http:\/\/afp.sf.net\/entries\/AVL-Trees.shtml"},{"key":"24_CR17","unstructured":"Peyton Jones, S.: Bulk types with class. In: FPW \u201996 (1996)"},{"key":"24_CR18","unstructured":"Stepanov, A., Lee, M.: The standard template library. Technical Report 95-11(R.1), HP Laboratories (1995)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:22Z","timestamp":1619785042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}