{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:50:36Z","timestamp":1725742236091},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_11","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"116-132","source":"Crossref","is-referenced-by-count":18,"title":["Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[]}],"member":"297","reference":[{"unstructured":"Appel, A.W.: Efficient verified red-black trees (2011), \n                    \n                      http:\/\/www.cs.princeton.edu\/~appel\/papers\/redblack.pdf","key":"11_CR1"},{"unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: SEFM 2004, pp. 230\u2013239. IEEE Computer Society (2004)","key":"11_CR2"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-03359-9_12","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2009","unstructured":"Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 147\u2013163. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Chen, K., Hudak, P., Odersky, M.: Parametric type classes. In: LFP 1992, pp. 170\u2013181. ACM (1992)","key":"11_CR4","DOI":"10.1145\/141478.141536"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1017\/S0956796807006338","volume":"18","author":"D.A. Greve","year":"2008","unstructured":"Greve, D.A., Kaufmann, M., Manolios, P., Moore, J.S., Ray, S., Ruiz-Reina, J., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Funct. Program.\u00a018(1), 15\u201346 (2008)","journal-title":"J. Funct. Program."},{"key":"11_CR6","series-title":"LNCS","first-page":"100","volume-title":"ITP 2013","author":"F. Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Progr. Lang. Sys.\u00a028, 619\u2013695 (2006)","journal-title":"ACM Trans. Progr. Lang. Sys."},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle Collections Framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 339\u2013354. Springer, Heidelberg (2010)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 166\u2013182. Springer, Heidelberg (2012)"},{"unstructured":"Lescuyer, S.: Containers: a typeclass-based library of finite sets\/maps (2011), \n                    \n                      http:\/\/coq.inria.fr\/pylons\/contribs\/view\/Containers\/v8.3","key":"11_CR11"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-03359-9_22","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Lochbihler","year":"2009","unstructured":"Lochbihler, A.: Formalising FinFuns \u2013 generating code for functions as data from Isabelle\/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 310\u2013326. Springer, Heidelberg (2009)"},{"unstructured":"Lochbihler, A.: A Machine-Checked, Type-Safe Model of Java Concurrency: Language, Virtual Machine, Memory Model, and Verified Compiler. PhD thesis, Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik (2012)","key":"11_CR13"},{"unstructured":"Lochbihler, A.: Light-weight containers. Archive of Formal Proofs, Formal proof development (2013) \n                    \n                      http:\/\/afp.sf.net\/entries\/Containers.shtml","key":"11_CR14"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-642-22863-6_17","volume-title":"Interactive Theorem Proving","author":"A. Lochbihler","year":"2011","unstructured":"Lochbihler, A., Bulwahn, L.: Animating the formalised semantics of a Java-like language. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 216\u2013232. Springer, Heidelberg (2011)"},{"issue":"50","key":"11_CR16","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F. Mari\u0107","year":"2010","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci.\u00a0411(50), 4333\u20134356 (2010)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Peyton Jones, S.: Bulk types with class. In: Haskell Workshop 1997 (1997)","key":"11_CR17"},{"doi-asserted-by":"crossref","unstructured":"Svenningsson, J.: Shortcut fusion for accumulating parameters & zip-like functions. In: ICFP 2002, pp. 124\u2013132. ACM (2002)","key":"11_CR18","DOI":"10.1145\/583852.581491"},{"unstructured":"Thiemann, R.: Generating linear orders for datatypes. Archive of Formal Proofs, Formal proof development (2012), \n                    \n                      http:\/\/afp.sf.net\/entries\/Datatype_Order_Generator.shtml","key":"11_CR19"}],"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-39634-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T05:43:26Z","timestamp":1557985406000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}