ClassicThesis Dissertation

\documentclass[11pt,a4paper,twoside,openright]{scrbook}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[nochapters,beramono,eulermath,pdfspacing,dottedtoc]{classicthesis}
\usepackage[left=3cm,right=6cm,top=3cm,bottom=3cm,marginparwidth=4.5cm]{geometry}
\usepackage{graphicx}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}
\usepackage[backend=biber,style=authoryear,sorting=nyt]{biblatex}
\usepackage[colorlinks=true,linkcolor=Maroon,citecolor=Maroon,urlcolor=Maroon]{hyperref}

\addbibresource{references.bib}

\title{\rmfamily\normalfont\spacedallcaps{On the Foundations of Computational Reasoning}}
\author{\spacedlowsmallcaps{First Last}}
\date{\today}

\begin{document}
\frenchspacing
\raggedbottom
\pagenumbering{roman}
\pagestyle{plain}

\begin{titlepage}
  \vspace*{\fill}
  \begin{center}
    \rmfamily\Huge\spacedallcaps{On the Foundations of Computational Reasoning} \\[2em]
    \Large\spacedlowsmallcaps{A Dissertation Submitted to the Faculty} \\[0.5em]
    \Large\spacedlowsmallcaps{In Partial Fulfillment of the Requirements} \\[0.5em]
    \Large\spacedlowsmallcaps{for the Degree of Doctor of Philosophy} \\[4em]
    \Large\spacedlowsmallcaps{by} \\[1em]
    \Huge\spacedlowsmallcaps{First Last} \\[6em]
    \Large\spacedlowsmallcaps{Department of Computer Science} \\
    \Large\spacedlowsmallcaps{University of Example} \\[2em]
    \Large\today
  \end{center}
  \vspace*{\fill}
\end{titlepage}

\cleardoublepage
\pdfbookmark[1]{Abstract}{Abstract}
\chapter*{Abstract}
This thesis investigates the foundations of computational reasoning through
a unified lens combining type theory, category theory, and operational semantics.
We present a novel calculus and prove soundness, completeness, and decidability
of its core fragment. Extensive experiments show a 2.3x improvement over
prior art across six standard benchmarks.

\cleardoublepage
\pdfbookmark[1]{Acknowledgments}{Acknowledgments}
\chapter*{Acknowledgments}
I am grateful to my advisor, committee members, colleagues, and family.

\cleardoublepage
\pdfbookmark[1]{Contents}{toc}
\tableofcontents
\cleardoublepage

\pagenumbering{arabic}
\pagestyle{scrheadings}

\chapter{Introduction}
\label{ch:intro}
This dissertation addresses three central questions in computational reasoning.
\section{Motivation}
Modern software systems demand formal guarantees that current tools cannot provide.
\section{Contributions}
\begin{itemize}
  \item A new core calculus with provable meta-theoretic properties.
  \item An efficient decision procedure with optimal complexity.
  \item An open-source implementation evaluated on realistic workloads.
\end{itemize}

\chapter{Background}
\label{ch:background}
We recall standard definitions from lambda calculus and dependent type theory.
\begin{definition}[Reduction]
A term $t$ reduces to $t'$ if $t \to_\beta t'$ via the usual rules.
\end{definition}

\chapter{The Core Calculus}
\label{ch:calculus}
We introduce $\lambda_\square$, a calculus with explicit modality.
\begin{theorem}[Soundness]
If $\Gamma \vdash t : \tau$ and $t \to t'$, then $\Gamma \vdash t' : \tau$.
\end{theorem}
\begin{proof}
By induction on the derivation of $\Gamma \vdash t : \tau$.
\end{proof}

\chapter{Implementation}
\label{ch:impl}
The implementation is approximately 8{,}000 lines of OCaml.

\chapter{Evaluation}
\label{ch:eval}
\begin{table}[h]
  \centering
  \caption{Benchmark results.}
  \begin{tabular}{lrr}
    \toprule
    Benchmark & Prior (s) & Ours (s) \\
    \midrule
    parity   & 12.4 & 5.1 \\
    boolring & 18.9 & 7.8 \\
    prime    & 24.1 & 10.2 \\
    \bottomrule
  \end{tabular}
\end{table}

\chapter{Related Work}
\label{ch:related}
We position our contributions relative to prior work on session types,
refinement types, and dependent types.

\chapter{Conclusion}
\label{ch:conclusion}
We have shown that the core calculus is both sound and complete,
and that the implementation is practical.

\cleardoublepage
\printbibliography

\end{document}