We propose a rich foundational theory of typed data streams and stream transformers, motivated by two high-level goals: (1) the type of a stream should be able to express complex sequential patterns of events over time, and (2) it should describe the parallel structure of the stream to enable deterministic stream processing on parallel and distributed systems. To this end, we introduce stream types, with operators capturing sequential composition, parallel composition, and iteration, plus a core calculus of transformers over typed streams which naturally supports a number of common streaming idioms, including punctuation, windowing, and parallel partitioning, as first-class constructions. The calculus exploits a Curry-Howard-like correspondence with an ordered variant of the logic of Bunched Implication to program with streams compositionally and uses Brzozowski-style derivatives to enable an incremental, event-based operational semantics. To validate our design, we provide a reference interpreter and machine-checked proofs of the main results.

翻译：我们提出了一种关于类型化数据流和流转换器的丰富基础理论，其动机源于两个高层次目标：（1）流的类型应能够表达事件随时间变化的复杂序列模式；（2）它应描述流的并行结构，从而在并行和分布式系统上实现确定性流处理。为此，我们引入了流类型，其运算符捕获了顺序组合、并行组合和迭代，以及一种基于类型化流的转换器核心演算，该演算自然支持多种常见的流处理惯用模式，包括标点、窗口化和并行分区，并将其视为一等构造。该演算利用了一种类似于柯里-霍华德对应的关系，与束蕴含逻辑的有序变体相结合，以实现流的组合式编程，并使用布佐佐夫斯基风格的导数来实现增量式、基于事件的操作语义。为了验证我们的设计，我们提供了一个参考解释器以及主要结果的机器验证证明。