Calculating Compilers for Concurrency

Patrick Bahr, Graham Hutton

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationProceedings of the ACM on Programming Languages
Number of pages28
Place of PublicationNew York, NY, USA
Publication date31 Aug 2023
Article number213
Publication statusPublished - 31 Aug 2023


  • program calculation
  • choice trees
  • concurrency
  • codensity monad


Dive into the research topics of 'Calculating Compilers for Concurrency'. Together they form a unique fingerprint.

Cite this