Functional Meaning for Parallel Streaming
summary
A core language called λ∨ formalizes deterministic parallel streaming by making values monotonically increase under a streaming order that matches Scott approximation; the paper gives a denotational model using domain theory, solves the domain equation with a horror power domain for sets, and proves computational adequacy via a filter-model/type-system-style logical relation. Programs like an infinite evens set and a two‑phase commit are encoded using a parallel join operator that streams results and composes nodes deterministically in the infinite limit.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:21Nondeterminism in parallelism
- 1:25Shared state with semi lattices
- 2:11Lambda join for streaming
- 3:13New approach to deterministic parallelism
- 3:34Evens function example
- 6:41Two-phase commit algorithm
- 9:29Lambda join for fixed-point
- 10:33Operational semantics for infinite data
- 12:16Denotational semantics proof
- 13:20Domain theory insights
- 14:03Future work on distributed systems
- 14:45Incremental evaluation efficiency
- 15:07Aggregation and PageRank
- 15:28Conclusion
- 15:50Q&A
related talks
17mFlo: a Semantic Foundation for Progressive Stream Processing
26mA Framework for Adversarial Streaming via Differential Privacy and Difference Estimators
19mWe Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
44mUnderstanding Distributed Calculi in Haskell
01h 32mDistributed functional programming
01h 11mA Programmable Cloud: CALM Foundations and Open Challenges
32mMaximizing Throughput and Scalability for Akka Streams
46mPropagators