Tachis: Higher-Order Separation Logic with Credits for Expected Costs

on YouTube ↗17m

" summary

Tachis introduces probabilistic cost credits, a separation logic resource that preserves expectation across random branches and lets proofs allocate credits proportionally to sampling weights. It verifies concrete bounds: coin toss uses 2 ticks expected, randomized quicksort gets expected O(n log n) without solving recurrences, a batching trick reduces entropy from 8 bits per flip to amortized 1 bit per flip, and meldable heaps meet expected logarithmic costs. All proofs are formalized with a Coq/Iris/Coquelicot mechanization.

AI-written summary · about

" chapters (10)

1. 0:00TACIS introduction and goals
2. 1:46Time credits in separation logic
3. 3:33Time credits in probabilistic programs
4. 4:57Fixing time credits for expected costs
5. 6:01TACIS contributions summary
6. 8:30Expected cost rule details
7. 8:50Verifying QuickSort in TACIS
8. 11:17Coin flipping with entropy costs
9. 14:04K-way merge with randomized heaps
10. 15:48Conclusion and Q&A