@article{calcon,
  author = {Patrick Bahr and Graham Hutton},
  title = {Calculating Compilers for Concurrency},
  abstract = {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.},
  issue_date = {August 2023},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {7},
  number = {ICFP},
  journal = {Proceedings of the ACM on Programming Languages},
  month = aug,
  Date = {2023-08-31},
  articleno = {213},
  numpages = {28},
  url = {https://doi.org/10.1145/3607855},
  doi = {10.1145/3607855},
  Keywords = {program calculation, verified compiler, virtual machine, Agda, bisimulation, monad, choice trees},
  year = {2023}
}