流类型
摘要：关于类型化数据流和流变换器的丰富基础理论：类型化数据流的类型应该能够表达随时间变化的复杂顺序事件模式，并且应该描述流的并行结构以支持在并行和分布式系统上进行确定性流处理。为了达到这个目标，我们引入了流类型，其中运算符捕获了顺序组合、并行组合和迭代，还有一个基于类型化流的转换器的核心演算，自然地支持了一些常见的流式编码风格，包括标点符号、窗口化和并行分区，作为一流的构造。这个演算利用了一种与Bunched Implication逻辑的顺序变体类似的Curry-Howard对应关系，可以使流的编程具有组合性，并使用了Brzozowski风格的导数，以实现增量、基于事件的操作语义。为了验证我们的设计，我们提供了一个参考解释器，并对主要结果进行了机器验证的证明。
作者：Joseph W. Cutler, Christopher Watson, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, Benjamin C. Pierce
论文ID：2307.09553
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-20