{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:09Z","timestamp":1767928509044,"version":"3.49.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>Choice trees have recently been introduced as a general structure \nfor defining the semantics of programming languages with a wide variety \nof features and effects. In this article we focus on concurrent languages, \nand show how a codensity version of choice trees allows the semantics \nfor such languages to be systematically transformed into compilers using \nequational reasoning techniques. The codensity construction is the key \ningredient that enables a high-level, algebraic approach. As a case \nstudy, we calculate a compiler for a concurrent lambda calculus with \nchannel-based communication.<\/jats:p>","DOI":"10.1145\/3607855","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"740-767","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Calculating Compilers for Concurrency"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1600-8261","authenticated-orcid":false,"given":"Patrick","family":"Bahr","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9584-5150","authenticated-orcid":false,"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_2_1_2_1","volume-title":"Department of Computer Science","author":"Ager Mads Sig","unstructured":"Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. 2003. From Interpreter to Compiler and Virtual Machine: A Functional Derivation. BRICS, Department of Computer Science, University of Aarhus."},{"key":"e_1_2_1_3_1","volume-title":"Calculating Correct Compilers. Journal of Functional Programming, 25","author":"Bahr Patrick","year":"2015","unstructured":"Patrick Bahr and Graham Hutton. 2015. Calculating Correct Compilers. Journal of Functional Programming, 25 (2015)."},{"key":"e_1_2_1_4_1","volume-title":"Calculating Correct Compilers II: Return of the Register Machines. Journal of Functional Programming, 30","author":"Bahr Patrick","year":"2020","unstructured":"Patrick Bahr and Graham Hutton. 2020. Calculating Correct Compilers II: Return of the Register Machines. Journal of Functional Programming, 30 (2020)."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the ACM on Programming Languages, 6, ICFP","author":"Bahr Patrick","year":"2022","unstructured":"Patrick Bahr and Graham Hutton. 2022. Monadic Compiler Calculation. Proceedings of the ACM on Programming Languages, 6, ICFP (2022)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Patrick Bahr and Graham Hutton. 2023. Supplementary Material for \u201cCalculating Compilers for Concurrency\u201d. https:\/\/doi.org\/10.5281\/zenodo.8124116 10.5281\/zenodo.8124116","DOI":"10.5281\/zenodo.8124116"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Ale\u0161 Bizjak Hans Grathwohl Ranald Clouston Rasmus M\u00f8gelberg and Lars Birkedal. 2016. Guarded Dependent Type Theory with Coinductive Types. In Foundations of Software Science and Computation Structures.","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"e_1_2_1_8_1","volume-title":"General Recursion via Coinductive Types. Logical Methods in Computer Science, 1, 2","author":"Capretta Venanzio","year":"2005","unstructured":"Venanzio Capretta. 2005. General Recursion via Coinductive Types. Logical Methods in Computer Science, 1, 2 (2005)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571254"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005192"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364546"},{"key":"e_1_2_1_13_1","unstructured":"2023. The Science of Deep Specification. https:\/\/deepspec.org\/"},{"key":"e_1_2_1_14_1","volume-title":"The Art, Science, and Engineering of Programming, 6, 2","author":"Gibbons Jeremy","year":"2021","unstructured":"Jeremy Gibbons. 2021. Continuation-Passing Style, Defunctionalization, Accumulations, and Associativity. The Art, Science, and Engineering of Programming, 6, 2 (2021)."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_16"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the International Conference on Certified Programs and Proofs.","author":"He Paul","year":"2020","unstructured":"Chung-kil Hur, Paul He, Yannick Zakowski, and Steve Zdancewic. 2020. An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction. In Proceedings of the International Conference on Certified Programs and Proofs."},{"key":"e_1_2_1_17_1","volume-title":"Concurrent Haskell. In Proceedings of the Symposium on Principles of Programming Languages.","author":"Jones Simon Peyton","year":"1996","unstructured":"Simon Peyton Jones, Andrew Gorden, and Sigbjorn Finne. 1996. Concurrent Haskell. In Proceedings of the Symposium on Principles of Programming Languages."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science.","author":"Kristensen Magnus","year":"2022","unstructured":"Magnus Kristensen, Rasmus Mogelberg, and Andrea Vezzosi. 2022. Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction Under Clocks. In Proceedings of the Symposium on Logic in Computer Science."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_23_1","volume-title":"Formal Verification of a Realistic Compiler. Commun. ACM, 52, 7","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM, 52, 7 (2009)."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the ACM on Programming Languages, 3, ICFP","author":"Patterson Daniel","year":"2019","unstructured":"Daniel Patterson and Amal Ahmed. 2019. The Next 700 Compiler Correctness Theorems. Proceedings of the ACM on Programming Languages, 3, ICFP (2019)."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_1_26_1","volume-title":"A Unified View of Monadic and Applicative Non-Determinism. Science of Computer Programming, 152","author":"Rivas Exequiel","year":"2018","unstructured":"Exequiel Rivas, Mauro Jaskelioff, and Tom Schrijvers. 2018. A Unified View of Monadic and Applicative Non-Determinism. Science of Computer Programming, 152 (2018), Jan.."},{"key":"e_1_2_1_27_1","volume-title":"Formalizing CCS and \u03c0 -calculus in Guarded Cubical Agda. Journal of Logical and Algebraic Methods in Programming, 131","author":"Veltri Niccol\u00f2","year":"2023","unstructured":"Niccol\u00f2 Veltri and Andrea Vezzosi. 2023. Formalizing CCS and \u03c0 -calculus in Guarded Cubical Agda. Journal of Logical and Algebraic Methods in Programming, 131 (2023)."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_20"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357179"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582179"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224193"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","author":"Zakowski Yannick","year":"2019","unstructured":"Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2019. Interaction Trees: Representing Recursive and Impure Programs in Coq. Proceedings of the ACM on Programming Languages, 4, POPL (2019)."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547630"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607855","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607855","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":34,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607855"],"URL":"https:\/\/doi.org\/10.1145\/3607855","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}