Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

Explore a groundbreaking 20-minute video presentation from POPL 2024 introducing Trillium, a novel separation logic framework for intensional refinement in concurrent and distributed systems. Delve into how this language-agnostic approach strengthens higher-order separation logic to prove complex safety and liveness properties. Learn about Fairis, a concurrent separation logic built on Trillium, and its application in demonstrating liveness properties under fair scheduling. Discover how Trillium extends to distributed systems through an enhancement of Aneris logic, enabling refinement relations with TLA+ models. Gain insights into the potential of intensional refinement for overcoming limitations in step-indexing and expanding the scope of provable properties in program logics.

[POPL'24] Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...