Choice trees have recently been introduced as a general structure for defining the semantics of 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.

@article{paperbot1914,
  title = {Calculating Compilers for Concurrency},
  author = {Patrick Bahr and Graham Hutton},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {ICFP},
  year = {2023},
  doi = {10.1145/3607855}
}