A Spontaneous ICFP Submission Appears

We’ve just (well, last Friday) submitted a paper to ICFP! Our paper is about completeness proofs for Iris. Specifically, we develop a general method for showing that Iris Program Logics are complete, which is to say that they can verify any correct closed program; thus there are no accidentally forgotten rules. You can read more about it in the pre-print.

What is crazy about this paper is that three weeks ago, none of it existed. I had a very preliminary Rocq proof and vague dreams about submitting a 6- or 16-page paper to ITP. Somehow, I found some amazing coauthors and together we managed to push out six (!) case studies, strengthen and generalize our approach, and write a 25-page paper within less than three weeks. Thanks to Zichen, Joe, Puming, Simon and of course Ralf for the incredibly efficient collaboration.

What an international collaboration between China, the US, and Europe looks like in practice.

I might write a blog post where I talk more about the backstory of this paper and/or about completeness and why you should care about it. Subscribe to my RSS feed if you don’t want to miss it, or follow me on Mastodon.