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.

Categories: Compilers, Formal Verification

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