Layers of Confluence for Actors
summary
Presents a concrete proof technique that adapts de Bruijn’s induction-style confluence proof to indexed transition systems and a weak diamond property (D1/D2) so layered actor programs become provably confluent even without strong confluence or commutativity. Method is fully mechanised in Rocq (1.5k–4k LOC proofs), uses static call-graph analysis and purity/termination constraints on methods, and ships artifacts; main deliverable is constructive closure lemmas that close the critical call-order peak for layered and single-server call graphs.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:24Motivating example
- 2:05Confluence limits
- 3:31Transition systems
- 8:03Mechanized proof in Rocq
- 10:52Applying theory
- 15:07Purity assumptions
- 16:32Lambda act classes
- 19:01Conclusion
- 20:48Q&A
related talks
19mScenario-based Proofs for Concurrent Objects
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
24mFrom Enhanced Coinduction towards Enhanced Induction
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
28mReasoning about Distributed Reconfigurable Systems
41mTowards language support for distributed systems
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr