Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.

Simon Spies, Lennard Gher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal

Browse the full PLDI paper archive.