paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Fusing Session-Typed Concurrent Programming into Functional Programming

将会话类型并发编程融入函数式编程
ICFP 9(ICFP)2025匹配度 1/10 · 该论文属于纯编程语言理论与类型系统方向,研究函数式编程与会话类型并发进程的融合,未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析,与用户研究画像的核心交叉方向无直接关联。引用 2 inbox
Chuta Sano, Deepak Garg, Ryan Kavanagh, Brigitte Pientka, Bernardo Toninho
crossref: 2026-09-10

AI 速览

一句话:提出 FuSes,将函数式编程与会话类型并发进程演算融合,并支持类型安全元编程优化。

论文提出 FuSes,一种将会话类型并发进程演算代码融入函数式编程的语言。其架构是函数层位于会话类型进程层之上:函数层通过扩展了线性通道上下文的 contextual box 模态来生成并推理开放会话类型进程;由于两层操作语义存在根本差异,FuSes 提供原语在函数层内运行和观察封闭进程的行为。它还支持对开放会话类型进程代码的分析与操纵,并能以类型安全的元程序实现批处理等已知优化。技术贡献包括 FuSes 的类型系统、操作语义、类型安全性证明和实现。

问题
函数式层的操作语义与会话类型进程层的并发语义存在根本差异,如何在同一语言中安全融合并推理开放与封闭的会话类型进程代码。
方法
设计分层语言 FuSes:函数层位于会话类型进程层之上,使用扩展线性通道上下文的 contextual box 模态处理开放进程,并提供运行、观察封闭进程的原语及代码分析与元编程支持。
评估
给出类型系统、操作语义与类型安全性证明,并实现 FuSes 原型;以类型安全元程序实现批处理优化等案例展示其对程序员的益处。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}