% Compiler proof
%   Structure of proof, and high-level discussion
%   Technical devices: structured traces, labelling, etc.
%   Assembler proof
%   Technical issues in front end (Brian?)
%   Main theorem statement

\section{Compiler proof}
\label{sect.compiler.proof}