Composing Correctness Proofs

Planned post. This page is a stub.

Connecting machine instructions to an abstract interface.

Planned Coverage

Compose representation relations and lift single-call results to sequences of calls.

Examples, definitions, and exercises will be developed here as the course progresses. See the course table of contents for the suggested reading order.