ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States

Choice trees have recently been introduced as a general structure for giving semantics to programming languages with a wide variety of features and effects. In this article we focus on concurrent languages, and show how a codensity version of choice trees allows the semantics for such languages to be systematically transformed into compilers using equational reasoning techniques. The codensity construction is the key ingredient that enables a high-level, algebraic approach. As a case study, we calculate a compiler for a concurrent lambda calculus with channel-based communication.