  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 internal parallel structure of the stream to support
deterministic stream processing on parallel and distributed systems. To these
ends, we introduce stream types, with operators capturing sequential
composition, parallel composition, and iteration, plus a core calculus
lambda-ST of transformers over typed streams which naturally supports a number
of common streaming idioms, including punctuation, windowing, and parallel
partitioning, as first-class constructions. lambda-ST 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, prefix-based operational
semantics. To illustrate the programming style supported by the rich types of
lambda-ST, we present a number of examples written in delta, a prototype
high-level language design based on lambda-ST.
