{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:57:39Z","timestamp":1725857859492},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_38","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"568-577","source":"Crossref","is-referenced-by-count":6,"title":["Translating Scala Programs to Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Lars","family":"Hupel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"38_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Scala Workshop (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"38_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Heidelberg (2014)"},{"key":"38_CR4","unstructured":"Breitner, J., Huffman, B., Mitchell, N., Sternagel, C.: Certified HLints with Isabelle\/HOLCF-Prelude, Haskell and Rewriting Techniques (HART), June 2013"},{"key":"38_CR5","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"key":"38_CR6","doi-asserted-by":"crossref","unstructured":"Haftmann, F.: From higher-order logic to Haskell: there and back again. In: Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 155\u2013158. ACM (2010)","DOI":"10.1145\/1706356.1706385"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"38_CR8","unstructured":"Haller, P., Prokopec, A., Miller, H., Klang, V., Kuhn, R., Jovanovic, V.: Futures and promises (2012). http:\/\/docs.scala-lang.org\/overviews\/core\/futures.html"},{"issue":"4","key":"38_CR9","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2009","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303\u2013336 (2009)","journal-title":"J. Autom. Reason."},{"key":"38_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/978-3-319-17524-9_2","volume-title":"NASA Formal Methods","author":"V Kuncak","year":"2015","unstructured":"Kuncak, V.: Developing verified software using Leon. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 12\u201315. Springer, Heidelberg (2015)"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O.: Correctness of Isabelle\u2019s cyclicity checker: implementability of overloading in proof assistants. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, pp. 85\u201394. ACM, New York (2015)","DOI":"10.1145\/2676724.2693175"},{"key":"38_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"518","DOI":"10.1007\/978-3-642-20398-5_42","volume-title":"NASA Formal Methods","author":"H Mehnert","year":"2011","unstructured":"Mehnert, H.: Kopitiam: modular incremental interactive full functional static verification of java code. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 518\u2013524. Springer, Heidelberg (2011)"},{"key":"38_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"38_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics. Springer, New York (2014)"},{"key":"38_CR15","volume-title":"Programming in Scala","author":"M Odersky","year":"2010","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala, 2nd edn. Artima Inc, Walnut Creek (2010)","edition":"2"},{"key":"38_CR16","unstructured":"Terdoslavich, W.: IBM bets on apache spark as \u2019the future of enterprise data\u2019. http:\/\/www.informationweek.com\/big-data\/ibm-bets-on-apache-spark-as-the-future-of-enterprise-data\/d\/d-id\/1320855"},{"key":"38_CR17","doi-asserted-by":"crossref","unstructured":"Voirol, N., Kneuss, E., Kuncak, V.: Counter-example complete verification for higher-order functions. In: Scala Symposium (2015)","DOI":"10.1145\/2774975.2774978"},{"key":"38_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/978-3-642-22673-1_17","volume-title":"Intelligent Computer Mathematics","author":"M Wenzel","year":"2011","unstructured":"Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 244\u2013259. Springer, Heidelberg (2011)"},{"key":"38_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"468","DOI":"10.1007\/978-3-642-31374-5_38","volume-title":"Intelligent Computer Mathematics","author":"M Wenzel","year":"2012","unstructured":"Wenzel, M.: Isabelle\/jEdit \u2013 a prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 468\u2013471. Springer, Heidelberg (2012)"},{"key":"38_CR20","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual (2013)"},{"key":"38_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-319-08970-6_33","volume-title":"Interactive Theorem Proving","author":"M Wenzel","year":"2014","unstructured":"Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle\/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515\u2013530. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:12:45Z","timestamp":1498306365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}