Cutting the Cake: A Language for Fair Division
summary
A domain-specific language called Slice DSL encodes cake-cutting protocols and compiles them to logical constraints that are sound and complete with respect to the semantics; a prototype emits SMT formulas and verifies envy-freeness with Z3 SMT solver. The implementation automatically checks several classical protocols, returning results under <1s per protocol for all but the most complex (≈20s), and includes proofs, formal semantics, and artifact links for reproducibility.
AI-written summary · about
chapters (15)
- 0:00Fair cake division intro
- 1:07Envy-free basics
- 3:20Cake-cutting history
- 4:43Protocol challenges
- 5:26Modeling cake and allocations
- 6:30Agent valuations and interactions
- 7:36Introducing Slice language
- 9:00Protocols to constraints
- 10:49Verifying envy freeness
- 11:54Future directions
- 13:20Q&A: Contiguity
- 14:21Q&A: Practical challenges
- 15:04Q&A: Higher dimensions
- 16:11Q&A: Formal vs natural
- 17:16Q&A: Tool improvements
related talks
22mImplementing separation logic using an SMT-backed Frame Rule
15mDo You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
35mDesigning Domain-Specific Languages: A Comparison of Three Approaches by Example
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
18mBaking for Dafny: A CakeML Backend for Dafny
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
24mDesigning a DSL That Perfectly Solves Your Problem
41mConcatenative programming and stack-based languages