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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the ACM on Programming Languages |
| Number of pages | 28 |
| Volume | 7 |
| Place of Publication | New York, NY, USA |
| Publication date | 31 Aug 2023 |
| Pages | 740–767 |
| Article number | 213 |
| DOIs | |
| Publication status | Published - 31 Aug 2023 |
Keywords
- program calculation
- choice trees
- concurrency
- codensity monad
Fingerprint
Dive into the research topics of 'Calculating Compilers for Concurrency'. Together they form a unique fingerprint.Datasets
-
Supplementary Material for "Calculating Compilers for Concurrency"
Bahr, P. (Creator) & Hutton, G. (Creator), ZENODO, 31 May 2023
DOI: 10.5281/zenodo.8124116, https://zenodo.org/record/8124116
Dataset: Software