{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:08:02Z","timestamp":1781258882789,"version":"3.54.1"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T00:00:00Z","timestamp":1591401600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T00:00:00Z","timestamp":1591401600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"UK Research Institute in Verified Trustworthy Software Systems"},{"name":"A*STAR National Science Scholarship (PhD), Singapore"},{"DOI":"10.13039\/501100001729","name":"Swedish Foundation for Strategic Research","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001729","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I\/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.<\/jats:p>","DOI":"10.1007\/s10817-020-09559-8","type":"journal-article","created":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T02:02:17Z","timestamp":1591408937000},"page":"1287-1306","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Proof-Producing Synthesis of CakeML from Monadic HOL Functions"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4861-2650","authenticated-orcid":false,"given":"Oskar","family":"Abrahamsson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Son","family":"Ho","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hrutvik","family":"Kanabar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ramana","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yong Kiam","family":"Tan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,6,6]]},"reference":[{"key":"9559_CR1","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":"9559_CR2","unstructured":"Anand, A., Boulier, S., Tabareau, N., Sozeau, M.: Typed template Coq\u2014certified meta-programming in Coq. In: CoqPL (2018)"},{"key":"9559_CR3","doi-asserted-by":"crossref","unstructured":"Blazy, S., Robillard, B., Appel, A.W.: Formal verification of coalescing graph-coloring register allocation. In: ESOP, Volume 6012 of LNCS (2010)","DOI":"10.1007\/978-3-642-11957-6_9"},{"key":"9559_CR4","doi-asserted-by":"crossref","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.A., Tahar, S. (eds.) TPHOLs, Volume 5170 of LNCS, pp. 134\u2013149 (2008)","DOI":"10.1007\/978-3-540-71067-7_14"},{"key":"9559_CR5","doi-asserted-by":"crossref","unstructured":"Gu\u00e9neau, A., Myreen, M.O., Kumar, R., Norrish, M.L.: Verified characteristic formulae for CakeML. In: Yang, H. (ed.) ESOP, Volume 10201 of LNCS, pp. 584\u2013610 (2017)","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"9559_CR6","doi-asserted-by":"crossref","unstructured":"Ho, S., Abrahamsson, O., Kumar, R., Myreen, M.O., Tan, Y.K., Norrish, M.: Proof-producing synthesis of CakeML with I\/O and local state from monadic HOL functions. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR, pp. 646\u2013662 (2018)","DOI":"10.1007\/978-3-319-94205-6_42"},{"key":"9559_CR7","doi-asserted-by":"crossref","unstructured":"Hupel, L., Nipkow, T.: A verified compiler from Isabelle\/HOL to CakeML. In: Ahmed, A. (ed.) European Symposium on Programming (ESOP). Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"9559_CR8","doi-asserted-by":"crossref","unstructured":"Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM, Volume 6617 of LNCS, pp. 177\u2013191 (2011)","DOI":"10.1007\/978-3-642-20398-5_14"},{"issue":"3","key":"9559_CR9","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."},{"key":"9559_CR10","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Suresh, J., Sewell, P. (eds.) POPL, pp. 179\u2013192 (2014)","DOI":"10.1145\/2578855.2535841"},{"key":"9559_CR11","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Refinement to Imperative\/HOL. In: ITP, Volume 9236 of LNCS (2015)","DOI":"10.1007\/978-3-319-22102-1_17"},{"key":"9559_CR12","doi-asserted-by":"crossref","unstructured":"Launchbury, J., Peyton Jones, S.L.: Lazy functional state threads. In: Sarkar, V., Ryder, B.G., Soffa, M.L. (eds.) PLDI, pp. 24\u201335 (1994)","DOI":"10.1145\/773473.178246"},{"key":"9559_CR13","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)","DOI":"10.1145\/3167089"},{"issue":"2\u20133","key":"9559_CR14","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":"9559_CR15","doi-asserted-by":"crossref","unstructured":"Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP, Volume 9632 of LNCS, pp. 589\u2013615 (2016)","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"9559_CR16","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09559-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09559-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09559-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,5]],"date-time":"2021-06-05T23:25:16Z","timestamp":1622935516000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09559-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,6]]},"references-count":16,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["9559"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09559-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,6]]},"assertion":[{"value":"21 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}