Towards Session-Typed Consensus
summary
Attempts to encode Raft in MAGπ show the calculus models non-Byzantine faults, asynchronous messaging, undirected branching and timeouts but fails to enforce Raft’s essential term numbers: types allow well-formed messages and leader-election exchanges (request-vote, ack, majority promotion) yet cannot prevent promoting on stale votes. The paper proposes a minimal conservative extension adding rounds/terms into session types and explores realizations via refinement, dependent-like checks or epistemic modalities.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:07Typing consensus algorithms
- 3:00Consensus challenges
- 5:09Session types vs consensus
- 7:16Magpie calculus for failures
- 9:46Raft consensus demo
- 10:50Raft leader election
- 12:56Session typing leader election
- 15:20Session typing limitations
- 17:31Dependent and refinement typing
- 19:39Summary and discussion
- 20:02Raft with shared session types
- 22:51Type guarantees vs practicality
- 24:38Future protocol verification
- 25:43Q&A: Applied pi calculus
- 26:26Q&A: Code generation
- 27:32Q&A: Round-based verification
- 29:18Closing remarks
related talks
47mUnderstanding Raft Consensus
01h 32mHow to Reach Consensus with Paper, Pencil and the Raft Algorithm
01h 27mHow to Reach Consensus Using Paper, Pencil and the Raft Algorithm
41mThe Raft Consensus Algorithm
14mDistributed Consensus in 15 Minutes!
47mDistributed Systems: When Democracy and Computer Science Come Together
01h 13mPaxos vs Raft: Have we reached consensus on distributed consensus?
51mDo Not Reimplement Distributed Consensus Algorithms