thesis.tex

%%%%%
%%
%% thesis.tex --- Mechanized Finite Domain Decision Procedures
%%
%% Built on the University of Cambridge cam-thesis class (v0.2).
%% Structure: one folder per chapter under chapters/, each acting as a
%% self-contained paper repo (chapter tex + plots/ + images/).
%% Package loading lives in packages.sty; thesis-wide macros in macros.sty.
%%%%%

\PassOptionsToPackage{dvipsnames}{xcolor}

% Available documentclass options:
%
%   <all `report` document class options, e.g.: `a5paper`>
%   withindex   - enables the index. New index entries can be added through `\index{my entry}`
%   glossary    - enables the glossary.
%   techreport  - typesets the thesis in the technical report format.
%   firstyr     - formats the document as a first-year report.
%   times       - uses the `Times` font.
%   backrefs    - add back references in the Bibliography section
%
% For more info see `README.md`
%% cam-thesis.cls loads microtype itself, so expansion has to be passed in
%% before the class runs; \microtypesetup after the fact is too late to affect
%% fonts the class has already selected.
\PassOptionsToPackage{expansion=alltext}{microtype}
\documentclass[withindex,glossary]{cam-thesis}

% Citations using numbers
\usepackage[numbers]{natbib}

\usepackage{packages}
\usepackage{macros}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Thesis meta-information
%%

\title{Mechanized Decision Procedures for Compiler Verification}
\author{Siddharth Bhat}
\college{Churchill College}
\collegeshield{CollegeShields/Churchill}

%% Submission date [optional]:
% \submissiondate{November, 2042}

%% Declaration date:
\date{July 2026}

%% PDF meta-info:
\subjectline{Computer Science}
\keywords{decision procedures, bitvectors, floating point, Lean, SMT, compiler verification}

% Minted setup (Lean/MLIR/xDSL environments and custom lexers) lives in macros.sty.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Abstract and acknowledgements (separate files under frontmatter/):
%%
\abstract{\input{frontmatter/abstract}}
\acknowledgements{\input{frontmatter/acknowledgements}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Glossary [optional]:
%%
\newglossaryentry{HOL}{
    name=HOL,
    description={Higher-order logic}
}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Contents:
%%
\begin{document}

%% Title page, abstract, declaration, acknowledgements, table of contents:
%% The frontmatter carries no margin captions and no marginal chapter numbers,
%% so the wide caption margin of the body would just read as an off-centre
%% text block -- most visibly on the title page. Set these pages on symmetric
%% margins (the same numbers as the ToC geometry in packages.sty); the
%% asymmetric wide-margin layout starts with the introduction.
\newgeometry{a4paper, twoside=false, left=20mm, right=20mm, top=25mm,
             bottom=25mm, marginparwidth=12mm, marginparsep=4mm}
\frontmatter{}
\restoregeometry

%% Running heads. cam-thesis.cls leaves the body on \pagestyle{plain} -- a bare
%% outer page number and nothing else. classicthesis has already configured
%% scrlayer-scrpage for its own headline style (spaced small caps: chapter
%% title on the verso, numbered section title on the recto, with the page
%% number hung outboard in the margin); it just is not switched on. Do that
%% here rather than in the class, which is upstream code.
%%
%% `plain' stays in force on chapter-opening pages via scrheadings' plain
%% variant, so the \ofoot page number there is unaffected.
\pagestyle{scrheadings}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Thesis body: one folder per chapter.
%%
\input{chapters/introduction/introduction}
\input{chapters/background/background}
\input{chapters/lean-mlir/lean-mlir}
\input{chapters/background-bv/background-bv}
\input{chapters/parametric-bv/pbv-preamble}
\input{chapters/single-width-bv/mono-width-bv}
\input{chapters/multi-width-bv/multi-width-bv}
\input{chapters/floating-point/floating-point}
\input{chapters/future-work/future-work}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Appendix:
%%
\appendix
% \input{chapters/appendix-artefacts/artefacts}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% References:
%%
\renewcommand{\bibname}{References}
\cleardoublepage
\phantomsection
\addcontentsline{toc}{chapter}{References}
\bibliographystyle{plainnat}
\bibliography{thesis}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Index:
%%
\printthesisindex

\end{document}