Follow
New blog post: the Gradual Guarantee via step-indexed logical relations (in Agda)
https://siek.blogspot.com/2023/05/gradual-guarantee-via-step-indexed.html
@maxsnew thanks! Yes, I'll be in town and will be happy to talk.
@jeremysiek this is very cool Jeremy I've got a student working on a similar approach where we're using Guarded Cubical Agda rather than implementing our own guarded logic. We should chat about it sometime. I'm going to be in Bloomington for MFPS the week of June 19 are you going to be around at all?