{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:13Z","timestamp":1762459633005},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319942049"},{"type":"electronic","value":"9783319942056"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94205-6_42","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T12:22:50Z","timestamp":1530274970000},"page":"646-662","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Proof-Producing Synthesis of CakeML with I\/O and Local State from Monadic HOL Functions"],"prefix":"10.1007","author":[{"given":"Son","family":"Ho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oskar","family":"Abrahamsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramana","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong Kiam","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"unstructured":"Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Belanger, O.S., Sozeau, M., Weaver, M.: CertiCoq: a verified compiler for Coq. In: CoqPL (2017)","key":"42_CR1"},{"unstructured":"Anand, A., Boulier, S., Tabareau, N., Sozeau, M.: Typed template Coq - certified meta-programming in Coq. In: CoqPL (2018)","key":"42_CR2"},{"key":"42_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-642-11957-6_9","volume-title":"Programming Languages and Systems","author":"S Blazy","year":"2010","unstructured":"Blazy, S., Robillard, B., Appel, A.W.: Formal verification of coalescing graph-coloring register allocation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 145\u2013164. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_9"},{"key":"42_CR4","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. 5170, pp. 134\u2013149. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_14"},{"key":"42_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1007\/978-3-662-54434-1_22","volume-title":"Programming Languages and Systems","author":"A Gu\u00e9neau","year":"2017","unstructured":"Gu\u00e9neau, A., Myreen, M.O., Kumar, R., Norrish, M.: Verified characteristic formulae for CakeML. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 584\u2013610. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_22"},{"key":"42_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"999","DOI":"10.1007\/978-3-319-89884-1_35","volume-title":"Programming Languages and Systems","author":"L Hupel","year":"2018","unstructured":"Hupel, L., Nipkow, T.: A verified compiler from Isabelle\/HOL to CakeML. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 999\u20131026. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_35"},{"key":"42_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-20398-5_14","volume-title":"NASA Formal Methods","author":"J Hurd","year":"2011","unstructured":"Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177\u2013191. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_14"},{"issue":"3","key":"42_CR8","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-015-9357-x","volume":"56","author":"R Kumar","year":"2016","unstructured":"Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: Self-formalisation of higher-order logic - semantics, soundness, and a verified implementation. J. Autom. Reason. 56(3), 221\u2013259 (2016)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 179\u2013192 (2014)","key":"42_CR9","DOI":"10.1145\/2535838.2535841"},{"key":"42_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-22102-1_17","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2015","unstructured":"Lammich, P.: Refinement to imperative\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253\u2013269. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_17"},{"doi-asserted-by":"crossref","unstructured":"Launchbury, J., Jones, S.L.P.: Lazy functional state threads. In: Sarkar, V., Ryder, B.G., Soffa, M.L. (eds.) PLDI, pp. 24\u201335 (1994)","key":"42_CR11","DOI":"10.1145\/178243.178246"},{"doi-asserted-by":"crossref","unstructured":"Mullen, E., Pernsteiner, S., Wilcox, J.R., Tatlock, Z., Grossman, D.: \u0152uf: minimizing the Coq extraction TCB. In: CPP (2018)","key":"42_CR12","DOI":"10.1145\/3176245.3167089"},{"issue":"2\u20133","key":"42_CR13","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1017\/S0956796813000282","volume":"24","author":"MO Myreen","year":"2014","unstructured":"Myreen, M.O., Owens, S.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2\u20133), 284\u2013315 (2014)","journal-title":"J. Funct. Program."},{"key":"42_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-49498-1_23","volume-title":"Programming Languages and Systems","author":"S Owens","year":"2016","unstructured":"Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 589\u2013615. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_23"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","key":"42_CR15","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T01:24:02Z","timestamp":1571534642000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}