一句话：提出时间化会话类型，给出判定合规性与构造最精确合规对端（及子类型可判定性）的可靠完备技术。
该文研究如何在会话类型中刻画带时间约束的通信协议。已有工作（未时间化的会话类型）以基于进展的合规关系描述两个参与者能否安全交互，但无法表达时序与超时。作者定义时间化会话类型，用以形式化会话两端之间的定时通信协议，并给出一个可判定的合规关系，将基于进展的合规性推广到时间场景。核心结果是一套可靠且完备的判定技术：可判定某个时间化会话类型是否存在与其合规的对端类型；在此基础上，依据合规关系诱导的子类型预序，构造出与给定类型合规的最精确会话类型，子类型的可判定性亦由此推出。摘要未报告实现或实验评估，贡献为理论层面的判定性与构造性结果。
Timed session types formalise timed communication protocols between two participants at the endpoints of a session. They feature a decidable compliance relation, which generalises to the timed setting the progress-based compliance between untimed session types. We show a sound and complete technique to decide when a timed session type admits a compliant one. Then, we show how to construct the most precise session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BartolettiCM17,
title = {Timed Session Types},
author = {Massimo Bartoletti and Tiziana Cimoli and Maurizio Murgia},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:25)2017}
}