@misc{indiciae9bdd4497b4e9, title = {Gradual Guarantee via Step-Indexed Logical Relations in Agda}, author = {Jeremy G. Siek}, year = {2024}, doi = {10.4204/eptcs.413.3}, url = {https://arxiv.org/abs/2412.03125}, note = {Source identifier: 2412.03125} }