Fusing Session-Typed Concurrent Programming into Functional Programming
We introduce FuSes, a Functional programming language that integrates Session-typed concurrent process calculus code. A functional layer sits on top of a session-typed process layer. To generate and reason about open session-typed processes, the functional layer uses the contextual box modality extended with linear channel contexts. Due to the fundamental differences between the operational semantics of the functional layer and the concurrent semantics of processes, we bridge the two layers using a set of primitives to run and observe the behavior of closed processes within the functional layer. In addition, FuSes supports code analysis and manipulation of open session-typed process code. To showcase its benefit to programmers we implement well-known optimizations as type-safe metaprograms over concurrent processes such as batch optimizations.
Our technical contributions include a type system for FuSes, an operational semantics, a proof of its type safety, and its implementation.
Wed 15 OctDisplayed time zone: Perth change
10:50 - 12:05 | |||
10:50 25mTalk | Fusing Session-Typed Concurrent Programming into Functional Programming ICFP Papers Chuta Sano McGill University, Deepak Garg MPI-SWS, Ryan Kavanagh Université du Québec à Montréal, Brigitte Pientka McGill University, Bernardo Toninho Instituto Superior Técnico - University of Lisbon DOI | ||
11:15 25mTalk | Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs ICFP Papers Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University DOI Pre-print | ||
11:40 25mTalk | Relax! The Semilenient Core of Choreographic Programming (Functional Pearl) ICFP Papers Dan Plyukhin University of Southern Denmark, Xueying Qin University of Southern Denmark, Fabrizio Montesi University of Southern Denmark DOI Pre-print | ||