一句话:提出 FuSes,将函数式编程与会话类型并发进程演算融合,并支持类型安全元编程优化。
论文提出 FuSes,一种将会话类型并发进程演算代码融入函数式编程的语言。其架构是函数层位于会话类型进程层之上:函数层通过扩展了线性通道上下文的 contextual box 模态来生成并推理开放会话类型进程;由于两层操作语义存在根本差异,FuSes 提供原语在函数层内运行和观察封闭进程的行为。它还支持对开放会话类型进程代码的分析与操纵,并能以类型安全的元程序实现批处理等已知优化。技术贡献包括 FuSes 的类型系统、操作语义、类型安全性证明和实现。
We introduce FuSes , a Fu nctional programming language that integrates Ses sion-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, such as batch optimizations, as type-safe metaprograms over concurrent processes. Our technical contributions include a type system for FuSes , an operational semantics, a proof of its type safety, and an implementation.
@article{paperbot3062,
title = {Fusing Session-Typed Concurrent Programming into Functional Programming},
author = {Chuta Sano and Deepak Garg and Ryan Kavanagh and Brigitte Pientka and Bernardo Toninho},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747519}
}