Machine Execution in Lean

Planned post. This page is a stub.

Registers, memory, instructions, and an executable RISC semantics.

Planned Coverage

Run a short instruction sequence and state the assumptions of its machine model.

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