{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:00:56Z","timestamp":1765666856355},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_22","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"310-326","source":"Crossref","is-referenced-by-count":7,"title":["Formalising FinFuns \u2013 Generating Code for Functions as Data from Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","first-page":"230","volume-title":"Proc. SEFM 2004","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Proc. SEFM 2004, pp. 230\u2013239. IEEE Computer Society, Los Alamitos (2004)"},{"key":"22_CR2","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 \u2013 lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 19\u201336. Springer, Heidelberg (1999)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/3-540-60275-5_61","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"G. Collins","year":"1995","unstructured":"Collins, G., Syme, D.: A theory of finite maps. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol.\u00a0971, pp. 122\u2013137. Springer, Heidelberg (1995)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/10930755_12","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 188\u2013203. Springer, Heidelberg (2003)"},{"unstructured":"Haftmann, F., Nipkow, T.: A code generator framework for Isabelle\/HOL. Technical Report 364\/07, Dept. of Computer Science, University of Kaiserslautern (2007)","key":"22_CR6"},{"key":"22_CR7","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)"},{"unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre (1995)","key":"22_CR8"},{"key":"22_CR9","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 TOPLAS\u00a028, 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","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, vol.\u00a04130, pp. 589\u2013603. Springer, Heidelberg (2006)"},{"unstructured":"Lochbihler, A.: Jinja with threads. The Archive of Formal Proofs. Formal proof development (2007), \n                    \n                      http:\/\/afp.sf.net\/entries\/JinjaThreads.shtml","key":"22_CR11"},{"unstructured":"Lochbihler, A.: Type safe nondeterminism - a formal semantics of Java threads. In: FOOL 2008 (2008)","key":"22_CR12"},{"unstructured":"Lochbihler, A.: Code generation for functions as data. The Archive of Formal Proofs. Formal proof development (2009), \n                    \n                      http:\/\/afp.sf.net\/entries\/FinFun.shtml","key":"22_CR13"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/11541868_25","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"2005","unstructured":"Nipkow, T., Paulson, L.C.: Proof pearl: Defining functions over finite sets. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 385\u2013396. Springer, Heidelberg (2005)"},{"unstructured":"Nipkow, T., Pusch, C.: AVL trees. The Archive of Formal Proofs. Formal proof development (2004), \n                    \n                      http:\/\/afp.sf.net\/entries\/AVL-Trees.shtml","key":"22_CR15"},{"issue":"4","key":"22_CR16","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C. Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. Journal of Automatic Reasoning\u00a040(4), 327\u2013356 (2008)","journal-title":"Journal of Automatic Reasoning"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/11814771_41","volume-title":"Automated Reasoning","author":"C. Urban","year":"2006","unstructured":"Urban, C., Berghofer, S.: A recursion combinator for nominal datatypes implemented in Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 498\u2013512. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T08:35:25Z","timestamp":1552120525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}