paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On Sessions and Infinite Data

论会话与无限数据
LMCS vol.Volume 13, Issue 22017匹配度 1/10 · 论文属于纯 PL 理论中的会话类型与按名调用演算，关注类型系统保证规范化和进程推进，未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析。虽然属于程序语言理论，但不在用户当前 PL 与 AI 交叉的核心研究范围内。引用 7 inbox
Paula Severi, Luca Padovani, Emilio Tuosto, Mariangiola Dezani-Ciancaglini
并发、并行与内存模型类型系统
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：提出结合按名调用函数核心与会话通信的演算，类型系统保证表达式规范化与进程推进。

本文定义了一个新的演算，将按名调用（call-by-name）的函数核心与会话通信原语结合在一起，用于统一描述函数式计算与基于会话的进程通信。作者为该演算设计了一套类型规则，其核心结果是同时保证表达式的规范化（normalisation）和进程的推进（progress）。在证明这些性质时，论文揭示出求值策略与通信行为之间存在一种此前未预料到的交互。该工作为在无限数据背景下研究会话类型、通信安全与终止性提供了形式化基础。

问题
如何在一个演算中统一按名调用函数核心与会话通信原语，并由类型系统同时保证表达式规范化与进程推进。
方法
定义带会话通信原语的 call-by-name 演算，建立类型规则，并证明表达式的规范化与进程的 progress。
评估
通过类型系统证明展示规范化与推进性质，并分析求值策略与通信行为之间的交互。
原文摘要（Abstract）

We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a typing discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and communication.Comment: 39 pages 6 files including .bbl

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{SeveriPTD16,
  title = {On Sessions and Infinite Data},
  author = {Paula Severi and Luca Padovani and Emilio Tuosto and Mariangiola Dezani-Ciancaglini},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 2},
  year = {2017},
  doi = {10.23638/lmcs-13(2:9)2017}
}