paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Safe stream-based programming with refinement types

使用精化类型的安全流式编程
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 2/10 · 论文研究用精化类型检查异步流式程序的线程安全,属于 PL/类型系统与并发验证;但未涉及用户的 AI/LLM 交叉、浮点程序分析或贝叶斯程序分析等核心方向。虽然形式化与工程实现符合部分偏好,但研究问题与画像核心匹配度很低。引用 6 inbox
Benno Stein, Lazaro Clapp, Manu Sridharan, Bor-Yuh Evan Chang
crossref: 2026-09-12

AI 速览

一句话:提出用精化类型规约并检查异步流式程序的线程行为,避免与单线程 UI 等受限特性交互时的不安全。

流式编程将数据源抽象为可通过回调操作的值流,已成为处理交互式软件中异步数据源的流行范式。但其高层抽象削弱了开发者对程序控制流与数据流关系的推理能力。当异步流式代码与线程受限特性(如仅允许单线程访问 UI 的框架)交互时,问题尤为突出:流式构造的线程行为往往不直观,且文档不足。标题表明论文以精化类型(refinement types)为核心方法,旨在为流式编程提供安全性检查,约束线程行为及相关控制/数据流关系。不过,给出的摘要未说明具体类型规则、实现与评估结果。

问题
流式编程以回调和数据流抽象异步数据源,但高层抽象使开发者难以推理控制流与数据流关系,尤其在与限定单线程访问的 UI 框架交互时,流式构造的线程行为不直观且文档不足。
方法
标题表明论文采用精化类型(refinement types)作为核心方法,用于对流式程序的线程行为与数据/控制流关系进行建模和静态检查,以提供安全保障;摘要未展开具体类型规则或实现。
评估
摘要未给出评估方式与结果;因此无法从给定材料判断其实现、案例研究或实验设置。
原文摘要(Abstract)

In stream-based programming, data sources are abstracted as a stream of values that can be manipulated via callback functions. Stream-based programming is exploding in popularity, as it provides a powerful and expressive paradigm for handling asynchronous data sources in interactive software. However, high-level stream abstractions can also make it difficult for developers to reason about control- and data-flow relationships in their programs. This is particularly impactful when asynchronous stream-based code interacts with thread-limited features such as UI frameworks that restrict UI access to a single thread, since the threading behavior of streaming constructs is often non-intuitive and insufficiently documented.

链接与引用

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

BibTeX
@inproceedings{paperbot4788,
  title = {Safe stream-based programming with refinement types},
  author = {Benno Stein and Lazaro Clapp and Manu Sridharan and Bor-Yuh Evan Chang},
  booktitle = {ASE},
  year = {2018},
  doi = {10.1145/3238147.3238174}
}