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.
Thu 7 SepDisplayed time zone: Pacific Time (US & Canada) change
15:00 - 16:00
|Calculating Compilers for Concurrency
ICFP Papers and EventsDOI Pre-print
|Trustworthy Runtime Verification via Bisimulation (Experience Report)Experience Report
ICFP Papers and Events
Ryan Scott Galois, Inc., Mike Dodds Galois, Inc., Robert Dockins Amazon, Ivan Perez NASA Ames Research Center, Alwyn Goodloe NASA Langley Research CenterDOI Pre-print