Patrick Bahr IT University of Copenhagen

Calculating Compilers for Concurrency

Patrick Bahr, presenting joint work with Graham Hutton
28th ACM SIGPLAN International Conference on Functional Programming (ICFP 2023)


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.

Categories: Compilers, Formal Verification

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