Lecture 27: Conclusion

In order to stabilize what you've learned in the class, take some time to recall what you learned and organize it. This outline give you some keywords to help you remember the broad concepts you've seen.

Functional programs

Inductive data types, recursive functions

Proofs by induction, computation, and rewriting

Specifying (functional) abstract data types

Imperative programs

Hoare logic; weakest preconditions

Separation logic to deal with the heap; frame rule

Soundness theorem

Specifying heap-based abstract data types

Concurrent programs

Weakest precondition for Fork

Concurrent soundness theorem

Fractional permissions

Resource algebras and ghost state

Specifying concurrent abstract data types with HOCAP

Coq

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: understanding weakest preconditions, and Hoare triples in Coq

Iris Proof Mode tactics

GooseLang: connecting code to Goose model, writing specifications for Go functions