Summary of the class

In order to stabilize what you've learned in the class, take some time to recall what you learned and organize it. This outline gives you a concise summary of the topics we've covered.

Functional programs

Inductive data types, recursive functions

Proofs by induction, computation, and rewriting

Imperative programs

Hoare logic

Separation logic: separating conjunction, frame rule

Soundness of separation logic

Specifying abstract data types (representation predicates)

Concurrent programs

Fractional permissions

Ghost variables

Lock invariants

Concurrent soundness theorem

Specifying concurrent abstract data types with atomic updates

Rocq

Writing definitions and theorems

Writing proofs with tactics

Translating informal proof strategy to tactics

Interactive proofs: reading the context, finding existing lemmas

Separation logic in Iris: weakest preconditions and continuation-passing style for Hoare triples

Iris Proof Mode tactics

Perennial: specifying Go functions and methods; struct points-to facts; slice ownership