一句话：提出公平异步子类型并在线性逻辑中构建会话类型系统，保证良类型进程公平终止且无饥饿与孤儿消息。
本文研究异步会话类型理论，目标是在适当公平假设下保证良类型进程终止。公平终止蕴含无饥饿与无孤儿消息，即包括利用异步性提前发送的消息最终都会被消费。为此作者提出一种新的公平异步子类型关系，用于会话类型，且比已有子类型关系更宽松。该类型系统首次牢固建立在线性逻辑之上：把公平异步子类型作为线性逻辑切割与公理规则的自然推广，并通过一组交换转换和深层切割归约来建模异步通信。结果给出公平终止的保证以及与既有理论的粗细比较。
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2503-07273,
title = {Fair Termination of Asynchronous Binary Sessions},
author = {Luca Padovani and Gianluigi Zavattaro},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {2},
year = {2026},
doi = {10.1145/3803862}
}