New blog post: the Gradual Guarantee via step-indexed logical relations (in Agda)

@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?

@maxsnew thanks! Yes, I'll be in town and will be happy to talk.

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.