Calculating Compilers for Concurrency

Bahr, Patrick; Hutton, Graham

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.

Citation

Bahr, P., & Hutton, G. (2023). Calculating Compilers for Concurrency. Proceedings of the ACM on Programming Languages, 7(ICFP), 740-767. https://doi.org/10.1145/3607855

• Journal Article Type: Article
• Acceptance Date: Jun 27, 2023
• Online Publication Date: Aug 31, 2023
• Publication Date: Aug 30, 2023
• Deposit Date: Jun 28, 2023
• Publicly Available Date: Aug 30, 2023
• Journal: Proceedings of the ACM on Programming Languages
• Electronic ISSN: 2475-1421
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 7
• Issue: ICFP
• Pages: 740-767
• DOI: https://doi.org/10.1145/3607855
• Keywords: Safety, Risk, Reliability and Quality; Software
• Public URL: https://nottingham-repository.worktribe.com/output/22392081