{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:54:45Z","timestamp":1754484885614},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1007\/s10817-012-9260-7","type":"journal-article","created":{"date-parts":[[2012,9,26]],"date-time":"2012-09-26T00:30:34Z","timestamp":1348619434000},"page":"357-370","source":"Crossref","is-referenced-by-count":10,"title":["Proof Pearl\u2014A Mechanized Proof of GHC\u2019s Mergesort"],"prefix":"10.1007","volume":"51","author":[{"given":"Christian","family":"Sternagel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,9,26]]},"reference":[{"key":"9260_CR1","unstructured":"Filli\u00e2tre, J.C., Magaud, N.: Certification of sorting algorithms in the Coq system. In: Theorem Proving in Higher Order Logics: Emerging Trends (1999). http:\/\/www-sop.inria.fr\/croap\/TPHOLs99\/proceeding.html"},{"key":"9260_CR2","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming, FLOPS 2010, Lecture Notes in Computer Science, vol. 6009, pp. 103\u2013117. Springer (2010). doi: 10.1007\/978-3-642-12251-4_9","DOI":"10.1007\/978-3-642-12251-4_9"},{"issue":"4","key":"9260_CR3","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reasoning 44(4), 303\u2013336 (2010). doi: 10.1007\/s10817-009-9157-2","journal-title":"J. Autom. Reasoning"},{"key":"9260_CR4","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014a proof assistant for higher-order logic. In: Lecture Notes in Computer Science, vol. 2283. Springer (2002). doi: 10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9260_CR5","unstructured":"O\u2019Keefe, R.: A smooth applicative merge sort. Tech. rep., Department of Artificial Intelligence, University of Edinburgh (1982)"},{"key":"9260_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the Working Programmer","author":"LC Paulson","year":"1996","unstructured":"Paulson, L.C.: ML for the Working Programmer, 2nd edn. Cambridge University Press, New York (1996)","edition":"2"},{"key":"9260_CR7","unstructured":"Sternagel, C.: Efficient Mergesort. In: Klein, G., Nipkow, T., Paulson, L.C. (eds.) The Archive of Formal Proofs. http:\/\/afp.sf.net\/entries\/Efficient-Mergesort.shtml (2011, formal proof development)"},{"key":"9260_CR8","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, TPHOLs 2009, Lecture Notes in Computer Science, vol. 5674, pp. 452\u2013468. Springer (2009). doi: 10.1007\/978-3-642-03359-9_31","DOI":"10.1007\/978-3-642-03359-9_31"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9260-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T00:39:25Z","timestamp":1498005565000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9260-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,26]]},"references-count":8,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["9260"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9260-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,9,26]]}}}