Additional resources

A core resource is the course lecture notes, which include some explanations and references not tied to any specific lecture.

Coq

If you want more practice I encourage you to read Software Foundations beyond the assigned chapters, and even to do additional exercises.

This Tactics Cheatsheet is much more complete than the Ltac reference I wrote. As a reminder, you're allowed to use any tactic in Coq (unless specifically forbidden).

For std++ sets and maps in particular, Search doesn't work especially well, since the definitions are so general. There I recommend looking at the coqdoc documentation for finite sets and finite maps. I'll be putting together a tutorial on these as the class progresses.

The Coq reference manual can be helpful, if you know what you're looking for. You should specifically use the tactic reference if you're using a built-in Coq tactic.

The textbook Certified Programming with Dependent Types (CPDT) is excellent for many advanced topics.

The textbook Verified Functional Algorithms (part of Software Foundations) gives detailed examples of data structure proofs using purely functional code.

Go

We will be working with Go code in this class. It will help to have at least reading familiarity with Go, which you can get by following A Tour of Go (you only really need the Basics and Methods chapters).

To verify code, it must also be in the subset of Go supported by Goose. You'll mostly be verifying provided code so won't need to understand these restrictions, but if your project involves writing new code I'll work with you to help you write it in the Goose-supported subset.

Iris

Use the IPM documentation as a reference for the tactics.

The new Iris tutorial is a Software Foundations-style introduction to Iris. It does not use GooseLang, so programs will look different from this class, but the high-level program reasoning and low-level tactics are otherwise the same.

The lecture notes for Semantics of Type Systems at MPI explains Iris "on paper". However, some background in programming language theory is needed to skip to the part on Iris and understand it.

The Iris lecture notes from Aarhus University explain Iris "on paper", in a self-contained manner. However, there is no connection to Coq and some knowledge of logic is expected to understand the material.

Iris from the ground up is an excellent reference if you want to understand how Iris works internally (though way too much if you just want to use it).

While not Iris-specific, the CS 240 notes on program correctness give a fantastic introduction to invariants and writing specifications. (Don't be fooled by the fact that this is a 200-level classes: most discrete math classes don't cover this material, so it is likely to be new to you.)

Papers

These papers are directly relevant to the class:

• Separation Logic (CACM 2019)
• Separation Logic for Sequential Programs (ICFP 2020)
• A beginner's guide to Iris, Coq and separation logic (Indiana University Bachelor's Thesis, 2021)
• Interactive Proofs in Higher-Order Concurrent Separation Logic

These are interesting papers for verification more broadly:

• Formal verification of a realistic compiler (CACM 2009) (CompCert)
• IronFleet: Proving Practical Distributed Systems Correct (SOSP 2015)
• How Amazon Web Services Uses Formal Methods (CACM 2015)
• BP: Formal Proofs, the Fine Print and Side Effects (IEEE SecDev 2018)
• Simple High-Level Code For Cryptographic Arithmetic – With Proofs, Without Compromises (IEEE S&P 2019) (Fiat Crypto)