Understanding Distributed Calculi in Haskell
summary
Live Haskell code uses distributed-process (Cloud Haskell) to implement a master/ping/pong example that actually runs, exposing where send/receive semantics block and where type-safety matters. An attempted implementation of Lamport logical clocks compiles but fails at runtime until message protocol mismatches and untyped queues are fixed, motivating typed channels as a practical remedy. The limits of synchronous π-calculus appear when names and receive-capabilities are sent, so the Rho calculus / Rholang family is presented as the cleaner, reflective solution.
AI-written summary · about
chapters (14)
- 0:00Introduction to the talk
- 1:04Haskell tutorial
- 2:39Handling effects in Haskell
- 5:15Distributed programming
- 7:14Ping-pong example
- 11:57Formalizing distributed systems
- 13:53Lambda calculus basics
- 18:50Introduction to pi-calculus
- 21:55Pi-calculus syntax and rules
- 26:18Structural congruence
- 31:58Pi-calculus examples
- 35:15Type systems for distributed
- 39:24Advanced calculus topics
- 42:52Conclusion and references
related talks
01h 11mA Programmable Cloud: CALM Foundations and Open Challenges
20mFour Years of Embedded Haskell in Critical Real-Time Systems: Lessons and Insights
01h 02mHydroflow: A Compiler Target for Fast, Correct Distributed Programs
28mReasoning about Distributed Reconfigurable Systems
01h 32mDistributed functional programming
01h 06mTransient: Unrestricted Algebraic and Monadic Composability
36mConcurrent ML - The One That Got Away
45mTaming Distribution: Formal Protocols for Akka Typed