@inproceedings{spies-2021-transfinitex, series={PLDI ’21}, title={Transfinite Iris: resolving an existential dilemma of step-indexed separation logic}, url={http://dx.doi.org/10.1145/3453483.3454031}, DOI={10.1145/3453483.3454031}, booktitle={Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation}, publisher={ACM}, author={Spies, Simon and Gäher, Lennard and Gratzer, Daniel and Tassarotti, Joseph and Krebbers, Robbert and Dreyer, Derek and Birkedal, Lars}, year={2021}, month=June, pages={80–95}, collection={PLDI ’21} }