Patrick Bahr Associate Professor, IT University of Copenhagen

Calculating compilers for concurrency

Patrick Bahr and Graham Hutton
Submitted to ICFP 2023.


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.

Categories: Compilers, Formal Verification

Tags: Program Calculation, Verified Compiler, Virtual Machine, Agda, Bisimulation, Monad, Choice Trees