New blog post: the Gradual Guarantee via step-indexed logical relations (in Agda)
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.
@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?