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

Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco +4

Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent…