\documentclass{article}
\usepackage[a4paper, margin=1in]{geometry}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\begin{document}

\title{Quantum and Classical Registers\thanks{Supported by the ERC consolidator grant CerQuS (819317), the PRG team grant “Secure Quantum Technology” (PRG946) from the Estonian Research Council, and the Estonian Centre of Exellence in IT (EXCITE) funded by ERDF.}}
\author{Dominique Unruh}
\maketitle

\begin{abstract}
  A formalization of the theory of quantum and classical registers as
  developed by Unruh \cite{unruh21registers}. In a nutshell, a
  register refers to a part of a larger memory or system that can be
  accessed independently.  Registers can be constructed from other
  registers and several (compatible) registers can be composed. For
  more details, see \cite{unruh21registers}. This formalization
  develops both the generic theory of registers as well as specific
  instantiations for classical and quantum registers.
\end{abstract}

\bigskip
\bigskip

\begin{quote}
  \textbf{Note:} This document assumes familiarity with the theoretical background developed in \cite{unruh21registers}.
  \cite{unruh21registers} also describes this formalization and mentions some of the design choices and challenges.

  Some of the theories are autogenerated (\textit{Laws\_Classical}, \textit{Laws\_Quantum}, \textit{Laws\_Complement\_Quantum}).
  Use the Python script \textit{instantiate\_laws.py} to recreate them after changing any of the theories starting with \textit{Laws} or \textit{Axioms}.
  See \cite{unruh21registers} for an explanation of this mechanism and the reasons for it.
\end{quote}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

\bibliographystyle{alpha}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
