Fusing Session-Typed Concurrent Programming into Functional Programming
summary
FuSes embeds a session-typed process calculus inside a pure functional language and ships a formal type system with operational semantics and a machine-checked proof of type safety. It exposes first-class process code via a contextual box modality with linear channel contexts, provides a run primitive that performs one communication round and returns a value plus a continuation reference, and implements a prototype with artifacts showing type-safe code-generation and metaprogramming optimizations (e.g. batching) working end-to-end.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:07Adding concurrency approaches
- 2:53Interoperability proposal
- 5:44Session types duality
- 9:16Integrating session types
- 13:13Concurrent Fibonacci example
- 15:00Running processes functionally
- 18:54Summary and future
- 20:19Q&A
- 21:02Q&A: Message limits
- 22:04Q&A: Runtime behavior
- 23:55Q&A: Code primitives
related talks
30mFP²: Fully in-Place Functional Programming
31mFunction-Passing Style Typed, Distributed Functional Programming
41mAn Introduction to Functional Imperative Programming in Flix
33mEXPLAIN FP LIKE RICHARD FEYNMAN
57mThe Fun of Functional Programming Panel
26mTypes as First-Class Values in Fuzion (Extended Abstract)
42mFunctional Programming in 40 Minutes
14mFundamentalist Functional Programming