{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:12:18Z","timestamp":1775671938193,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","funder":[{"name":"Swedish Research Council, Sweden","award":["2021-05165"],"award-info":[{"award-number":["2021-05165"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779098","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"157-170","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Brack: A Verified Compiler for Scheme via CakeML"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-9371-3467","authenticated-orcid":false,"given":"Pascal Y.","family":"Lasnier","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1650-6340","authenticated-orcid":false,"given":"Jeremy","family":"Yallop","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9504-4107","authenticated-orcid":false,"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"},{"name":"University of Gothenburg, Gothenburg, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010016816429"},{"key":"e_1_3_2_1_4_1","unstructured":"Olivier Danvy. 2004. On Evaluation Contexts Continuations and the Rest of Computation. 02."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411206"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001535"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773202"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 5th International Symposium on Functional and Logic Programming (FLOPS \u201901)","author":"Danvy Olivier","unstructured":"Olivier Danvy and Lasse R. Nielsen. 2001. A Higher-Order Colon Translation. In Proceedings of the 5th International Symposium on Functional and Logic Programming (FLOPS \u201901). Springer-Verlag, Berlin, Heidelberg. 78\u201391. isbn:3540417397"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00733-8"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779419.1779436"},{"key":"e_1_3_2_1_11_1","volume-title":"Vincent Vialard, and Wolfgang Goerigk.","author":"Dold Axel","year":"2005","unstructured":"Axel Dold, Friedrich Wilhelm von Henke, Vincent Vialard, and Wolfgang Goerigk. 2005. A mechanically verified compiling specification for a realistic compiler."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_13"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385994"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_3_2_1_15_1","volume-title":"Friedman","author":"Felleisen Matthias","year":"1987","unstructured":"Matthias Felleisen and Daniel P. Friedman. 1987. Control operators, the SECD-machine, and the \u03bb-calculus. In Formal Description of Programming Concepts. https:\/\/api.semanticscholar.org\/CorpusID:57760323"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"e_1_3_2_1_17_1","first-page":"131","article-title":"Reasoning with continuations","volume":"86","author":"Felleisen Matthias","year":"1986","unstructured":"Matthias Felleisen, Daniel P Friedman, Eugene E Kohlbecker, and Bruce F Duba. 1986. Reasoning with continuations. In LICS. 86, 131\u2013141.","journal-title":"LICS."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_3_2_1_19_1","volume-title":"On Lisp: Advanced Techniques for Common Lisp","author":"Graham P.","year":"1994","unstructured":"P. Graham. 1994. On Lisp: Advanced Techniques for Common Lisp. Prentice Hall. isbn:9780130305527 lccn:93009047"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01128407"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93554"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591259"},{"key":"e_1_3_2_1_23_1","volume-title":"Myreen","author":"Kumar Ramana","year":"2018","unstructured":"Ramana Kumar, Eric Mullen, Zachary Tatlock, and Magnus O. Myreen. 2018. Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB. In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing, Cham. 362\u2013369. isbn:978-3-319-94821-8"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747413"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the 28th International Symposium on Practical Aspects of Declarative Languages (PADL \u201926)","author":"Lasnier Pascal Y.","unstructured":"Pascal Y. Lasnier, Jeremy Yallop, and Magnus O. Myreen. 2026. A One-Pass CPS Transform with Simulation on the Nose. In Proceedings of the 28th International Symposium on Practical Aspects of Declarative Languages (PADL \u201926). Springer Nature Switzerland, Cham."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/976571.976576"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000282"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485491"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990074"},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the Twelfth Computing: The Australasian Theory Symposium -","volume":"51","author":"Tian Ye Henry","year":"2006","unstructured":"Ye Henry Tian. 2006. Mechanically verifying correctness of CPS compilation. In Proceedings of the Twelfth Computing: The Australasian Theory Symposium - Volume 51 (CATS \u201906). Australian Computer Society, Inc., AUS. 41\u201351. isbn:1920682333"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014408032446"},{"key":"e_1_3_2_1_38_1","volume-title":"Silent Bugs Matter: A Study of Compiler-Introduced Security Bugs. In 32nd USENIX Security Symposium, USENIX Security 2023","author":"Xu Jianhao","year":"2023","unstructured":"Jianhao Xu, Kangjie Lu, Zhengjie Du, Zhu Ding, Linke Li, Qiushi Wu, Mathias Payer, and Bing Mao. 2023. Silent Bugs Matter: A Study of Compiler-Introduced Security Bugs. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, Joseph A. Calandrino and Carmela Troncoso (Eds.). USENIX Association, 3655\u20133672. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/xu-jianhao"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779098","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:54:19Z","timestamp":1775667259000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779098"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":39,"alternative-id":["10.1145\/3779031.3779098","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779098","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}