text:
\section{Additional Features} \label{sec:additional-features}

Apart from minor surface syntax enhancements, the following features of Tower{} are omitted from the formal grammar, and we use them to improve readability of the example programs in this paper:
\begin{itemize}
\item \emph{\lstinline{if-else} statements}. We lower this construct to single-branch \lstinline{if} statements in the core.
\item \emph{\lstinline{with-do} blocks}. The statement $\sWith{\ensuremath{s}_1}{\ensuremath{s}_2}$ lowers to $\sSeq{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\reverse{\ensuremath{s}_1}}$. That is, the statement in the \lstinline{with}-block is reversed after executing the statement in the \lstinline{do}-block. We provide this construct to easily uncompute temporary values. For example, to store $(\texttt{x1} + \texttt{x2}) + \texttt{x3}$ into \texttt{result}, instead of writing
\begin{lstlisting}[style=nonum]
let temp <- x1 + x2;
let result <- temp + x3;
let temp -> x1 + x2; /* uncompute temp */
\end{lstlisting}
one may more concisely write
\begin{lstlisting}[style=nonum]
with { let temp <- x1 + x2; }
do { let result <- temp + x3; }
\end{lstlisting}
\item \emph{Nested expressions}. In fact, Tower{} supports writing $(\texttt{x1} + \texttt{x2}) + \texttt{x3}$ even more concisely through nesting expressions. One may simply write:
\begin{lstlisting}[style=nonum]
let result <- x1 + x2 + x3;
\end{lstlisting}
The lowering of this construct uncomputes all temporary values generated by evaluating nested expressions after their use. Nesting is supported for all expressions other than function arguments and return values as functions may cause side effects.
\item \emph{Patterns}. Tower{} supports assigning to and un-assigning from patterns, such as tuples and literals, in addition to variables. For example, to project from a tuple, instead of writing
\begin{lstlisting}[style=nonum]
let x <- t.1;
let y <- x.1;
let y -> 0;
let z <- x.2;
let x -> (y, z); /* uncompute x */
let w <- t.2;
\end{lstlisting}
one may more concisely write
\begin{lstlisting}[style=nonum]
let ((0, z), w) <- t;
\end{lstlisting}
\item \emph{Built-in operations}. Tower{} supports additional unary and binary operators, such as comparisons, bitwise operators, and pointer arithmetic.
\item \emph{Default values}. The operator \lstinline{default<t>} constructs $\default{\ensuremath{\tau}}$, the default value for type \lstinline{t}.
\end{itemize}

\section{Background on Quantum Computation} \label{sec:background}

The following is an overview of key concepts in quantum computation relevant to this work. \citet{nielsen_chuang_2010} provide a comprehensive reference.

\paragraph{Qubit}
The basic unit of quantum information is the \emph{qubit}, a linear combination $\gamma_0 \ket{0} + \gamma_1 \ket{1}$ known as a \emph{superposition}, where $\ket{0}$ and $\ket{1}$ are \emph{basis states} and $\gamma_0, \gamma_1 \in \mathbb{C}$ are \emph{amplitudes} satisfying $\abs{\gamma_0}^2 + \abs{\gamma_1}^2 = 1$ describing relative weights of basis states. Examples of qubits include the classical zero bit $\ket{0}$, classical one bit $\ket{1}$, and the superposition states $\frac{1}{\sqrt{2}}{(\ket{0} + \ket{1})}$ and $\frac{1}{\sqrt{2}}{(i\ket{0} - \ket{1})}$.

\paragraph{Quantum State}
A $2^n$-dimensional \emph{quantum state} $\ket{\ensuremath{\psi}}$ is a superposition over $n$-bit strings. For example, $\frac{1}{\sqrt{2}}{(\ket{00}+\ket{11})}$ is a quantum state over 2 qubits.
Multiple qubits form a quantum state system by means of the tensor product $\otimes$, e.g. the state $\ket{01}$ is equal to the product $\ket{0} \otimes \ket{1}$. As is standard in quantum computing, we also use the notation $\ket{x, y}$ to represent $\ket{x} \otimes \ket{y}$.

\paragraph{Unitary Operators}
A \emph{unitary operator} $U$ is a linear operator on quantum states that preserves inner products and whose inverse is its Hermitian adjoint.
Examples of unitary operators include single-qubit \emph{quantum gates} such as:
\begin{itemize}
    \item X -- bit-flip (NOT) gate, which maps $\ket{0} \mapsto \ket{1}$ and vice versa;
    \item Z -- phase-flip gate, which leaves $\ket{0}$ unchanged and maps $\ket{1} \mapsto -\ket{1}$;
    \item H -- Hadamard gate, which maps $\ket{0} \mapsto \frac{1}{\sqrt{2}}{(\ket{0} + \ket{1})}$ and $\ket{1} \mapsto \frac{1}{\sqrt{2}}{(\ket{0} - \ket{1})}$.
\end{itemize}
Other examples include two-qubit gates, such as controlled-NOT, controlled-Z, and SWAP. The controlled gates perform NOT or Z on their target qubit if their control qubit is in state $\ket{1}$, and the SWAP gate swaps two qubits in a quantum state.

\paragraph{Measurement}
A quantum \emph{measurement} is a probabilistic operation over quantum states. When a qubit $\gamma_0 \ket{0} + \gamma_1 \ket{1}$ is measured,\footnote{In this work, we refer only to projective computational (i.e. 0/1) basis measurements.} the outcome is $\ket{0}$ with probability $\abs{\gamma_0}^2$ and $\ket{1}$ with probability $\abs{\gamma_1}^2$. Measuring a qubit within a quantum state causes the entire state to probabilistically assume one of two outcome states.
To define the outcomes of measuring the first qubit of $\ket{\ensuremath{\psi}}$, we first rewrite the state into the form $\ket{\ensuremath{\psi}} = \gamma_0 \ket{0} \otimes \ket{\ensuremath{\psi}_0}+ \gamma_1 \ket{1} \otimes \ket{\ensuremath{\psi}_1}$. Then, with probability $\abs{\gamma_0}^2$ the measurement outcome is $\ket{0} \otimes \ket{\ensuremath{\psi}_0}$, and with probability $\abs{\gamma_1}^2$ the outcome is $\ket{1} \otimes \ket{\ensuremath{\psi}_1}$.
Outcomes of measuring multiple qubits or qubits other than the first are defined analogously.

\paragraph{Random Access}

Quantum random-access memory (qRAM)\footnotemark{}~\citep{Giovannetti_2008} enables manipulating data at addresses in superposition.
\footnotetext{The abbreviation qRAM is not to be confused with the QRAM model of computation by~\citet{knill}.}
Let $k$ be the word size of the system.
The single-qubit \emph{quantum random-access gate} is defined to be the unitary operation~\citep{ambainis2003}:
\[
\ket{i, b, z_1, \ldots, z_m} \mapsto \ket{i, z_i, z_1, \ldots, z_{i-1}, b, z_{i+1}, \ldots, z_m}
\]
where $i$ is a $k$-bit integer, $b$ is a bit, and $\ket{z_i, \ldots, z_m}$ is the qRAM -- an array of $m$ qubits. The effect of this gate is to swap the data at position $i$ in the array $z$ with the data in the register $b$.

In this work, we utilize a multi-qubit random-access gate, in which $b$ and each $z_i$ is a $k$-bit string rather than a single bit, that may be implemented as a straightforward extension of leading qRAM proposals~\citep{Paler_2020,Arunachalam_2015,Matteo_2020}.
For ease of classical comparisons, reported time complexities in this work assume quantum random access takes constant time. An alternative assumption made by~\citet{ambainis2003,aaronson2019,bernstein2013,buhrman2021} would contribute an additional $O(\log m)$ factor for a qRAM of size $m$.

\section{Conclusion} \label{sec:conclusion}

Data structures establish abstractions over mathematical objects, such as lists and sets, that are taken for granted by algorithmicists and ubiquitous in classical programming. However, their quantum implementations must satisfy additional properties, and existing quantum programming frameworks to date have left their construction to the developer.

In this work, we introduce Tower{}, a language for quantum programming with data structures, and Boson{}, a memory allocator that operates in quantum superposition, along with Ground{}, a library of abstract data structures, including the first implementation of the set data structure satisfying the requirements laid out by quantum algorithms. We hope that the library will be useful for quantum developers and that Tower{} and Boson{} will lead to even more useful abstractions.

Unlocking the potential of quantum computation rests on our ability to leverage the accumulated wisdom of algorithm and software design while grappling with physical and practical constraints that are unfamiliar to classical developers. As we have shown, understanding classically-motivated principles of computing, such as history independence, allows us to build bridges to abstractions such as data structures that will enable scalable and accessible quantum software.

\section{Core \LangName{}{}: Reversible and Circuit-Based Semantics} \label{sec:core-semantics}

Core \LangName{}{} is an imperative programming language that enables quantum programming with random-access memory. The operational semantics of the language is fully reversible, enabling a program to execute forwards or backwards. A Core \LangName{}{} program admits \emph{inversion}, which syntactically transforms it into another program with reversed semantics. A program also admits a syntactic translation into a unitary quantum circuit. In~\Cref{sec:main-semantics}, we extend Core \LangName{}{} with inductive data types and recursion to produce Tower{}.

\subsection{Syntax}

The syntax of Core \LangName{}{} consists of types, values, expressions, and statements.
\begin{align*}
    \textsf{Type}\ \ensuremath{\tau} \Coloneqq{} & t \mid \ensuremath{()} \mid \ensuremath{\texttt{uint}} \mid \ensuremath{\texttt{bool}} \mid \tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2} \mid \tPtr{\ensuremath{\tau}} \\
    \textsf{Value}\ \ensuremath{v} \Coloneqq{} & x \mid \ensuremath{()} \mid \ePair{x_1}{x_2} \mid \vNum{n} \mid \ensuremath{\texttt{true}} \mid \ensuremath{\texttt{false}} \mid \vNull{\ensuremath{\tau}} \mid \vPtr{\ensuremath{\tau}}{p} \hspace{1em} (n \in \textsf{UInt}, p \in \textsf{Addr}) \\
    \textsf{Expression}\ \ensuremath{e} \Coloneqq{} & \ensuremath{v} \mid \eProj{1}{x} \mid \eProj{2}{x} \mid \eUnop{uop}{x} \mid \eBinop{x_1}{bop}{x_2} \\
    \textsf{Operator}\ uop \Coloneqq{} & \ensuremath{\texttt{not}} \mid \ensuremath{\texttt{test}} \hspace{2em} bop \Coloneqq{} \ensuremath{\texttt{\&\&}} \mid \ensuremath{\texttt{||}} \mid \ensuremath{\texttt{+}} \mid \ensuremath{\texttt{-}} \mid \ensuremath{\texttt{*}} \\
    \textsf{Statement}\ \ensuremath{s} \Coloneqq{} & \ensuremath{\texttt{skip}} \mid \sSeq{\ensuremath{s}_1}{\ensuremath{s}_2} \mid \sBind{x}{\ensuremath{e}} \mid \sUnbind{x}{\ensuremath{e}} \mid \sSwap{x_1}{x_2} \mid \sMemSwap{x_1}{x_2} \mid \sIf{x}{s}
\end{align*}
\paragraph{Types}
The types \ensuremath{\tau}{} are type variables $t$, unit, unsigned integers, Booleans, products, and pointers.

\paragraph{Values}
The language distinguishes syntactic values $\ensuremath{v}$, which are variables, unit, pairs of variables, numeric, boolean, and pointer literals. Numeric literals $n$ are elements of a set \textsf{UInt} of unsigned integers in the range $[0, 2^k - 1]$ and pointer literals $p$ are elements of a set \textsf{Addr} of addresses in the range $[1, 2^k - 1]$, where the parameter $k$ is the word size of the system.

\paragraph{Expressions}
Expressions $\ensuremath{e}$ are values, projections, and unary and binary operators. These operators are standard logical and arithmetic operators on booleans and integers. The operation $\ensuremath{\texttt{test}}$ tests whether an integer is equal to zero or a pointer is equal to null.

\paragraph{Statements}
Statements $\ensuremath{s}$ include $\ensuremath{\texttt{skip}}$, which has no effect, and composition $\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}$ of statements. The assignment statement $\sBind{x}{\ensuremath{e}}$ initializes a variable $x$ and evaluates $\ensuremath{e}$, storing the result in $x$. The un-assignment statement $\sUnbind{x}{\ensuremath{e}}$ is unique to reversible programming --- it evaluates $\ensuremath{e}$ in reverse to restore $x$ back to its default state, and discards $x$. The swap statement $\sSwap{x_1}{x_2}$ exchanges the contents of variables $x_1$ and $x_2$. The swap-with-memory statement $\sMemSwap{x_1}{x_2}$ exchanges the contents of memory at address $x_1$ with the contents of $x_2$. Finally, the statement $\sIf{x}{s}$ has the effect of $s$ whenever the condition $x$ is true.

\subsection{Type System}
\begin{figure}
\resizebox{\textwidth}{!}{
\parbox{1.1\textwidth}{
\begin{mathpar}
\inferrule[TV-Var]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}, x : \ensuremath{\tau}}{x}{\ensuremath{\tau}}}

\inferrule[TV-Pair]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\tau}_2}}{\hastype{\ensuremath{\Gamma}}{\ePair{x_1}{x_2}}{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}}

\inferrule[TV-Num]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vNum{n}}{\ensuremath{\texttt{uint}}}}

\inferrule[TV-Bool]{b \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\hastype{\ensuremath{\Gamma}}{b}{\ensuremath{\texttt{bool}}}}

\inferrule[TV-Null]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vNull{\ensuremath{\tau}}}{\tPtr{\ensuremath{\tau}}}}

\inferrule[TV-Ptr]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vPtr{\ensuremath{\tau}}{p}}{\tPtr{\ensuremath{\tau}}}}

\inferrule[TE-Proj]{\hastype{\ensuremath{\Gamma}}{x}{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}}{\hastype{\ensuremath{\Gamma}}{\eProj{i}{x}}{\ensuremath{\tau}_i}}

\inferrule[TE-Not]{\hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\texttt{bool}}}}{\hastype{\ensuremath{\Gamma}}{\eUnop{\ensuremath{\texttt{not}}}{x}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Test]{\hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\tau}} \\\\ \ensuremath{\tau} \in \{\ensuremath{\texttt{uint}}, \tPtr{\ensuremath{\tau}'}\}}{\hastype{\ensuremath{\Gamma}}{\eUnop{\ensuremath{\texttt{test}}}{x}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Lop]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\texttt{bool}}} \quad \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\texttt{bool}}} \\\\ bop \in \{\ensuremath{\texttt{\&\&}}, \ensuremath{\texttt{||}}\}}{\hastype{\ensuremath{\Gamma}}{\eBinop{x_1}{bop}{x_2}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Aop]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\texttt{uint}}} \quad \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\texttt{uint}}} \\\\ bop \in \{\ensuremath{\texttt{+}}, \ensuremath{\texttt{-}}, \ensuremath{\texttt{*}}\}}{\hastype{\ensuremath{\Gamma}}{\eBinop{x_1}{bop}{x_2}}{\ensuremath{\texttt{uint}}}}
\end{mathpar}
}}
\setlength{\abovecaptionskip}{5pt}
\setlength{\belowcaptionskip}{-.5\baselineskip}
\caption{Selected typing rules in Core \LangName{}{}. The full definition is presented in~\Cref{sec:full-semantics}.} \label{fig:core-types}
\end{figure}
\begin{figure}
\resizebox{\textwidth}{!}{
\parbox{1.1\textwidth}{
\begin{mathpar}
\inferrule[S-Skip]{\vphantom{\ensuremath{\Gamma}}}{\stmtok{\ensuremath{\Gamma}}{\ensuremath{\texttt{skip}}}{\ensuremath{\Gamma}}}

\inferrule[S-Seq]{\stmtok{\ensuremath{\Gamma}}{\ensuremath{s}_1}{\ensuremath{\Gamma}'} \\ \stmtok{\ensuremath{\Gamma}'}{\ensuremath{s}_2}{\ensuremath{\Gamma}''}}{\stmtok{\ensuremath{\Gamma}}{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\ensuremath{\Gamma}''}}

\inferrule[S-Assign]{\hastype{\ensuremath{\Gamma}}{\ensuremath{e}}{\ensuremath{\tau}} \\ x \notin \ensuremath{\Gamma}}{\stmtok{\ensuremath{\Gamma}}{\sBind{x}{e}}{\ensuremath{\Gamma}, x : \ensuremath{\tau}}}

\inferrule[S-UnAssign]{\hastype{\ensuremath{\Gamma}}{\ensuremath{e}}{\ensuremath{\tau}} \\ x \notin \ensuremath{\Gamma}}{\stmtok{\ensuremath{\Gamma}, x : \ensuremath{\tau}}{\sUnbind{x}{e}}{\ensuremath{\Gamma}}}

\inferrule[S-Swap]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\tau}}}{\stmtok{\ensuremath{\Gamma}}{\sSwap{x_1}{x_2}}{\ensuremath{\Gamma}}}

\inferrule[S-MemSwap]{\hastype{\ensuremath{\Gamma}}{x_1}{\tPtr{\ensuremath{\tau}}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\tau}}}{\stmtok{\ensuremath{\Gamma}}{\sMemSwap{x_1}{x_2}}{\ensuremath{\Gamma}}}

\inferrule[S-If]{\stmtok{\ensuremath{\Gamma}}{\ensuremath{s}}{\ensuremath{\Gamma}} \\ \hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\texttt{bool}}} \\ x \notin \modified{\ensuremath{s}}}{\stmtok{\ensuremath{\Gamma}}{\sIf{x}{s}}{\ensuremath{\Gamma}}}
\end{mathpar}
}}
\setlength{\abovecaptionskip}{5pt}
\setlength{\belowcaptionskip}{-.5\baselineskip}
\caption{Well-formation rules for statements in Core \LangName{}{}.} \label{fig:core-stmt-ok}
\end{figure}
The type system of Core \LangName{}{} assigns a type to a value or expression and determines whether a statement is well-formed and corresponds to a valid quantum program.

\paragraph{Typing}
In~\Cref{fig:core-types}, we define the typing judgments for values and expressions. A context $\ensuremath{\Gamma}$ is a mapping from variables $x$ to types $\ensuremath{\tau}$. The judgment $\hastype{\ensuremath{\Gamma}}{\ensuremath{v}}{\ensuremath{\tau}}$ states that under context $\ensuremath{\Gamma}$, the value $\ensuremath{v}$ has type $\ensuremath{\tau}$.
The judgment $\hastype{\ensuremath{\Gamma}}{\ensuremath{e}}{\ensuremath{\tau}}$ states that under $\ensuremath{\Gamma}$, the expression $\ensuremath{e}$ has type $\ensuremath{\tau}$.

In~\Cref{fig:core-stmt-ok}, we define the judgment $\stmtok{\ensuremath{\Gamma}}{\ensuremath{s}}{\ensuremath{\Gamma}'}$, stating that under $\ensuremath{\Gamma}$, statement $\ensuremath{s}$ is well-formed and yields new context $\ensuremath{\Gamma}'$. The statement $\ensuremath{\texttt{skip}}$ has no effect, and sequencing of $\ensuremath{s}_1$ and $\ensuremath{s}_2$ composes their effect on the context. Assignment $\sBind{x}{\ensuremath{e}}$ is well-defined when $\ensuremath{\Gamma}$ does not contain $x$, and produces a context giving $x$ the type of $\ensuremath{e}$. Un-assignment is the reverse, removing $x$ from the context. A swap requires its arguments to have the same type, and a swap with memory requires the first argument to be a pointer to the type of the second.

An \texttt{if}-statement requires its branch $\ensuremath{s}$ to have no net effect on the context. For reversibility, it requires the condition to be a Boolean that is not modified by $\ensuremath{s}$, as defined by the judgement:
\begin{alignat*}{5}
\modified{\ensuremath{\texttt{skip}}} &= \emptyset \quad & \modified{\sSwap{x_1}{x_2}} &= \{x_1, x_2\} \\
\modified{\sSeq{s_1}{s_2}} &= \modified{s_1} \cup \modified{s_2} \quad & \modified{\sMemSwap{x_1}{x_2}} &= \{x_2\} \\
\modified{\sBind{x}{e}} &= \modified{\sUnbind{x}{e}} = \{x\} \quad & \modified{\sIf{x}{s}} &= \modified{s}
\end{alignat*}
\subsection{Reversible Operational Semantics}

The operational semantics of Core \LangName{}{} describes reversible operations that may be lifted to act in superposition over a quantum state. The semantics specifies how the machine state evolves during program evaluation while preserving sufficient information to enable reversibility.

\paragraph{Machine State}
The semantics transitions over \emph{machine states} $\mstate{\ensuremath{s}, \ensuremath{R}, \ensuremath{M}}$. Machine states consist of a program $\ensuremath{s}$, a \emph{register file} $\ensuremath{R}$ mapping variables to values, and a \emph{memory} $\ensuremath{M}$ mapping addresses to values. The register file $\ensuremath{R}$ corresponds to the main quantum registers over which we may perform arbitrary gates, while the memory $\ensuremath{M}$ corresponds to the qRAM. We use $\regtypes{\ensuremath{R}}$ to denote the typing context formed by mapping each variable in $\ensuremath{R}$ to the type of the value stored.

\paragraph{Default Value}
The default value of a type $\ensuremath{\tau}$, denoted $\default{\ensuremath{\tau}}$, is the initial value of a variable of type $\ensuremath{\tau}$ and corresponds to a convenient memory representation of constant zeroes of appropriate size:
\begin{alignat*}{5}
\default{\ensuremath{()}} &= \ensuremath{()} \quad & \default{\ensuremath{\texttt{bool}}} &= \ensuremath{\texttt{false}} \quad & \default{\tPtr{\ensuremath{\tau}}} &= \vNull{\ensuremath{\tau}} \\
\default{\ensuremath{\texttt{uint}}} &= \vNum{0} \quad & \default{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}} &= \ePair{\default{\ensuremath{\tau}_1}}{\default{\ensuremath{\tau}_2}} &
\end{alignat*}
\paragraph{Forward Evaluation}
In~\Cref{fig:core-exp-eval}, we define the forward expression evaluation judgment \linebreak$\estep{\ensuremath{e}}{\ensuremath{R}}{x}{z}{\ensuremath{v}}$. This judgment states that expression $\ensuremath{e}$ evaluates to value $\ensuremath{v}$, which is stored in register $x$, whose initial state was $z$. This judgment maintains reversibility by ensuring that 1) $\ensuremath{e}$ is not destroyed by evaluation, 2) $\ensuremath{v}$ is stored into a particular location $x$, and 3) the initial state $z$ of variable $x$ is a constant that remains known after this operation.

\begin{figure}
\resizebox{\textwidth}{!}{
\parbox{1.1\textwidth}{
\begin{mathpar}
\inferrule[SE-Var]{\get{\ensuremath{R}}{x'} = \ensuremath{v} \\ \hastype{\cdot}{\ensuremath{v}}{\ensuremath{\tau}}}{\estep{x'}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}

\inferrule[SE-Pair]{\get{\ensuremath{R}}{x_1} = \ensuremath{v}_1 \\ \get{\ensuremath{R}}{x_2} = \ensuremath{v}_2 \\ \hastype{\cdot}{\ensuremath{v}_1}{\ensuremath{\tau}_1} \\ \hastype{\cdot}{\ensuremath{v}_2}{\ensuremath{\tau}_2}}{\estep{\ePair{x_1}{x_2}}{\ensuremath{R}}{x}{\ePair{\default{\ensuremath{\tau}_1}}{\default{\ensuremath{\tau}_2}}}{\ePair{\ensuremath{v}_1}{\ensuremath{v}_2}}}

\inferrule[SE-Val]{v \neq x' \\ v \neq (x_1, x_2) \\ \hastype{\cdot}{\ensuremath{v}}{\ensuremath{\tau}}}{\estep{\ensuremath{v}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}

\inferrule[SE-Proj]{\get{\ensuremath{R}}{x'} = \ePair{\ensuremath{v}_1}{\ensuremath{v}_2} \\ \hastype{\cdot}{\ensuremath{v}_i}{\ensuremath{\tau}}}{\estepline{\eProj{i}{x'}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}_i}}

\inferrule[SE-Not]{\get{\ensuremath{R}}{x'} = b \\ b \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\estepline{\eUnop{\ensuremath{\texttt{not}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{\neg b}}

\inferrule[SE-Lop]{\get{\ensuremath{R}}{x_1} = b_1 \\ \get{\ensuremath{R}}{x_2} = b_2 \\\\ bop \in \{\ensuremath{\texttt{\&\&}}, \ensuremath{\texttt{||}}\} \\ b_1, b_2 \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\estepline{\eBinop{x_1}{bop}{x_2}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{b_1\ bop\ b_2}}

\inferrule[SE-Aop]{\get{\ensuremath{R}}{x_1} = \vNum{n_1} \\ \get{\ensuremath{R}}{x_2} = \vNum{n_2} \\ bop \in \{\ensuremath{\texttt{+}}, \ensuremath{\texttt{-}}, \ensuremath{\texttt{*}}\}}{\estepline{\eBinop{x_1}{bop}{x_2}}{\ensuremath{R}}{x}{\vNum{0}}{\vNum{n_1\ bop\ n_2}}}
\end{mathpar}
}}
\caption{Selected forward step rules of expressions in Core \LangName{}{}. The full definition is presented in~\Cref{sec:full-semantics}.} \label{fig:core-exp-eval}
\end{figure}
\begin{figure}
\resizebox{\textwidth}{!}{
\parbox{1.1\textwidth}{
\begin{mathpar}
\inferrule[SS-SeqStep]{\sstep{\ensuremath{s}_1}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'_1}{\ensuremath{R}'}{\ensuremath{M}'}}{\sstep{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\ensuremath{R}}{\ensuremath{M}}{\sSeq{\ensuremath{s}'_1}{\ensuremath{s}_2}}{\ensuremath{R}'}{\ensuremath{M}'}}

\inferrule[SS-Assign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \estep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\sstep{\sBind{x}{\ensuremath{e}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}}

\inferrule[SS-UnAssign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \restep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\sstep{\sUnbind{x}{\ensuremath{e}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[SS-Swap]{\vphantom{\ensuremath{\Gamma}}}{\sstepline{\sSwap{x_1}{x_2}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_1, \ensuremath{v}_2}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_2, \ensuremath{v}_1}}{\ensuremath{M}}}

\inferrule[SS-MemSwapNull]{\get{\ensuremath{R}}{x_1} = \vNull{\ensuremath{\tau}}}{\sstep{\sMemSwap{x_1}{x_2}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[SS-MemSwapPtr]{\get{\ensuremath{R}}{x_1} = \vPtr{\ensuremath{\tau}}{p}}{\sstepline{\sMemSwap{x_1}{x_2}}{\subst{\ensuremath{R}}{x_2}{\ensuremath{v}}}{\subst{\ensuremath{M}}{p}{\ensuremath{v}'}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x_2}{\ensuremath{v}'}}{\subst{\ensuremath{M}}{p}{\ensuremath{v}}}}
\end{mathpar}
}}
\caption{Selected forward step rules of statements in Core \LangName{}{}. The full definition is presented in~\Cref{sec:full-semantics}.} \label{fig:core-stmt-step}
\end{figure}

The first evaluation rule specifies that evaluating a variable $x'$ copies its value into a destination variable $x$ that starts in default state.
The following three rules similarly specify copying a known constant $\ensuremath{v}$, or a pair of values, or one field of a pair, into $x$.
The rules for unary and binary operators update $x$ based on a criterion computed from the arguments, and the rule for arithmetic operators updates $x$ to an arithmetic result over the arguments.

\paragraph{Reverse Evaluation}
In~\Cref{sec:full-semantics}, we define the reverse expression evaluation judgment \linebreak$\restep{\ensuremath{e}}{\ensuremath{R}}{x}{z}{\ensuremath{v}}$. This judgment states that given the result $\ensuremath{v}$ of evaluating $\ensuremath{e}$, stored in variable $x$, we may reverse the evaluation of $\ensuremath{e}$ and restore $x$ back to its initial state $z$.
All rules defining this judgment are reverses of the rules defining the forward evaluation.

\paragraph{Forward Step}
In~\Cref{fig:core-stmt-step}, we define the forward statement step judgment $\sstep{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'}{\ensuremath{R}'}{\ensuremath{M}'}$. This judgment states that given machine state $\mstate{\ensuremath{R}, \ensuremath{M}}$, executing statement $\ensuremath{s}$ results in new machine state $\mstate{\ensuremath{R}', \ensuremath{M}'}$ and new statement $\ensuremath{s}'$ to be executed next.

The first two rules skip the $\ensuremath{\texttt{skip}}$ statement and execute sequences left to right. The rule $\sBind{x}{e}$ first allocates a variable $x$ in default state, and then forward evaluates $\ensuremath{e}$, storing the result $\ensuremath{v}$ into $x$. The rule for un-assignment $\sUnbind{x}{e}$ reverses the evaluation of $\ensuremath{e}$ to restore the state of $x$ from $\ensuremath{v}$ back to the default state, and then deallocates $x$. The rule for $\sSwap{x_1}{x_2}$ exchanges the values of $x_1$ and $x_2$ in $\ensuremath{R}$. The rule for swapping with memory at a null pointer has no effect. The rule to swap $x_2$ with memory at a valid pointer $p$ swaps the value of $x_2$ in $\ensuremath{R}$ with the contents of $\ensuremath{M}$ at address $p$. Finally, the two rules for \texttt{if} either transition to the body $\ensuremath{s}$ if the condition passes or to $\ensuremath{\texttt{skip}}$ if it fails.

\begin{figure}
\resizebox{\textwidth}{!}{
\parbox{1.1\textwidth}{
\begin{mathpar}
\inferrule[RS-SeqStep]{\rsstep{\ensuremath{s}_2}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'_2}{\ensuremath{R}'}{\ensuremath{M}'}}{\rsstep{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\ensuremath{R}}{\ensuremath{M}}{\sSeq{\ensuremath{s}_1}{\ensuremath{s}'_2}}{\ensuremath{R}'}{\ensuremath{M}'}}

\inferrule[RS-Assign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \restep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\rsstep{\sBind{x}{\ensuremath{e}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}}

\inferrule[RS-UnAssign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \estep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\rsstep{\sUnbind{x}{\ensuremath{e}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[RS-Swap]{\vphantom{\ensuremath{\Gamma}}}{\rsstepline{\sSwap{x_1}{x_2}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_1, \ensuremath{v}_2}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_2, \ensuremath{v}_1}}{\ensuremath{M}}}
\end{mathpar}
}}
\caption{Selected reverse step rules of statements in Core \LangName{}{}. The full definition is provided in~\Cref{sec:full-semantics}.} \label{fig:core-stmt-reverse}
\end{figure}

\paragraph{Reverse Step}
In~\Cref{fig:core-stmt-reverse}, we define the reverse statement step judgment $\rsstep{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'}{\ensuremath{R}'}{\ensuremath{M}'}$. This judgment states that given machine state $\mstate{\ensuremath{R}', \ensuremath{M}'}$, executing statement $\ensuremath{s}$ in reverse results in new machine state $\mstate{\ensuremath{R}, \ensuremath{M}}$ and new statement $\ensuremath{s}'$ to be executed next.

Its rules are the reverse of the forward step. Sequential statements execute from right to left. The roles of $\sBind{x}{e}$ and $\sUnbind{x}{e}$ are flipped, with the latter now evaluating $e$ forward and the former evaluating backward. Because the reverse of a swap operation is itself, the rules for swap statements are the same. Executing an \texttt{if} in reverse requires reversing its body.

\subsection{Soundness}

We now show that Core \LangName{}{} satisfies key soundness properties:
\begin{definition}[Valid Machine State]
    A machine state $\mstate{\ensuremath{s}, \ensuremath{R}, \ensuremath{M}}$ is \emph{valid} if and only if $\ensuremath{R}$ maps exactly the variables that are free in $\ensuremath{s}$ to well-typed values, and $\stmtok{\regtypes{\ensuremath{R}}}{\ensuremath{s}}{\ensuremath{\Gamma}}$ for some $\ensuremath{\Gamma}$.
\end{definition}

\begin{theorem}[Preservation]
    If $\mstate{\ensuremath{s}, \ensuremath{R}, \ensuremath{M}}$ is a valid machine state and $\sstep{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'}{\ensuremath{R}'}{\ensuremath{M}'}$, then $\mstate{\ensuremath{s}', \ensuremath{R}', \ensuremath{M}'}$ is a valid machine state.
\end{theorem}

\begin{proof}
    By induction over the forward operational semantics of Core \LangName{}{}.
\end{proof}

A valid machine state $\mstate{\ensuremath{s}, \ensuremath{R}, \ensuremath{M}}$ fails to make progress only if it must execute statement $\sUnbind{x}{e}$ where $\ensuremath{e}$ does not compute the value of $x$, i.e. $\ensuremath{R} = \subst{\ensuremath{R}'}{x}{\ensuremath{v}}$ and $\restep{\ensuremath{e}}{\ensuremath{R}'}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}$ fails to hold. We denote this condition $\sstepstuck{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}$ and fully define it in~\Cref{sec:full-semantics}.

\begin{theorem}[Progress]
    Given a valid machine state $\mstate{\ensuremath{s}, \ensuremath{R}, \ensuremath{M}}$, either $\ensuremath{s}$ is $\ensuremath{\texttt{skip}}$ or $\sstepstuck{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}$ or $\sstep{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'}{\ensuremath{R}'}{\ensuremath{M}'}$ for some $\ensuremath{s}', \ensuremath{R}', \ensuremath{M}'$.
\end{theorem}

\begin{proof}
    By induction over the definition of valid machine states.
\end{proof}

Reversed equivalents of progress and preservation may be stated and proved analogously.

\subsection{Program Inversion} \label{sec:program-inversion}
Given a program $\ensuremath{s}$, its syntactic \emph{inversion} $\reverse{\ensuremath{s}}$ is a program whose semantics are reversed:
{\small
\begin{alignat*}{5}
\reverse{\ensuremath{\texttt{skip}}} &= \ensuremath{\texttt{skip}} \quad & \reverse{\sBind{x}{e}} &= \sUnbind{x}{e} \quad  & \reverse{\sSwap{x_1}{x_2}} &= \sSwap{x_1}{x_2} \\
\reverse{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}} &= \sSeq{\reverse{\ensuremath{s}_2}}{\reverse{\ensuremath{s}_1}} \quad & \reverse{\sUnbind{x}{e}} &= \sBind{x}{e} \quad & \reverse{\sMemSwap{x_1}{x_2}} &= \sMemSwap{x_1}{x_2} \\
& & & & \reverse{\sIf{x}{\ensuremath{s}}} &= \sIf{x}{\reverse{\ensuremath{s}}}
\end{alignat*}}
The following theorem states that the forward semantics of a program is equivalent to the reverse semantics of its inversion, where we define $\mapsto^*$ to be the reflexive transitive closure of $\mapsto$.

\begin{theorem}[Invertibility]
    $\sstepstar{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}'}{\ensuremath{M}'}$ iff $\rsstepstar{\reverse{\ensuremath{s}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}'}{\ensuremath{M}'}$.
\end{theorem}

\begin{proof}
    By induction over the forward operational semantics of Core \LangName{}{}.
\end{proof}

\subsection{Quantum Circuit Semantics} \label{sec:circuit-semantics}

We now develop a semantics of Core \LangName{}{} that translates a program $\ensuremath{s}$ to a unitary quantum circuit in order to execute $\ensuremath{s}$ on a quantum computer.

\paragraph{Expression Semantics}
Given an expression $\ensuremath{e}$ whose forward operational semantics is defined as $\estep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}$, we lift it to a unitary gate $U_\ensuremath{e}$ that operates on register file $\ensuremath{R}$ and a new register $x$ and stores $\ensuremath{v}$ in this register, that is, $U_\ensuremath{e}\ket{\ensuremath{R}, \default{\ensuremath{\tau}}} = \ket{\ensuremath{R}, \ensuremath{v}}$. Each possible expression -- production of constant value, variable reference, projection from a pair, integer arithmetic, and Boolean logic -- can be implemented as a unitary gate manipulating $x$:

\begin{itemize}
    \item A constant value $v$ can be reversibly produced by applying the NOT gate on each bit of $x$ whose corresponding bit is set in the bit representation of $v$.
    \item A variable $x'$ may be reversibly copied into $x$ by applying the conditional-NOT gate on each bit in $x$ conditioned on the corresponding bit of $x'$.
    \item Projection is analogous to copying a variable, except only one field of the pair is copied.
    \item Integer arithmetic may be reversibly performed through circuit designs such as~\citet{draper2000addition,cheng2002,islam2009low}.
    \item Boolean logic may be embedded reversibly into NOT and Toffoli (controlled-controlled-NOT) gates, as established by \citet{Fredkin1982ConservativeL}.
\end{itemize}

\paragraph{Statement Semantics}

\newsavebox{\slashwire}
\savebox{\slashwire}{
\begin{quantikz}
    & \qwbundle{}
\end{quantikz}
}
\newcommand{\smash{\hspace{-0.6em}\raisebox{0.3em}{$\oset{\hspace{1.7em}\tiny k}{\usebox{\slashwire}}$}\hspace{-0.1em}}}{\smash{\hspace{-0.6em}\raisebox{0.3em}{$\oset{\hspace{1.7em}\tiny k}{\usebox{\slashwire}}$}\hspace{-0.1em}}}

\newsavebox{\tripwire}
\savebox{\tripwire}{
\begin{quantikz}
    & \qwbundle[alternate]{}
\end{quantikz}
}
\newcommand{\hspace{-0.6em}\raisebox{0.3em}{\usebox{\tripwire}}\hspace{-0.1em}}{\hspace{-0.6em}\raisebox{0.3em}{\usebox{\tripwire}}\hspace{-0.1em}}

\newsavebox{\skipcircuit}
\savebox{\skipcircuit}{
\begin{quantikz}
    \lstick{$\ket{\ensuremath{R}, \ensuremath{M}}$} & \rstick{$\ket{\ensuremath{R}, \ensuremath{M}}$} \qwbundle[alternate]{}
\end{quantikz}
}
\newsavebox{\assigncircuit}
\savebox{\assigncircuit}{
\begin{quantikz}
    \lstick{$\ket{\ensuremath{R}}$} & \gate[wires=2]{U_{\ensuremath{e}}}\qwbundle[alternate]{} & \rstick{$\ket{\ensuremath{R}}$} \qwbundle[alternate]{} \\
    \lstick{$\ket{0}^{\otimes k}$} & \qwbundle{\hspace{-1em}k} & \rstick{$\ket{x}$} \qwbundle{k}
\end{quantikz}
}
\newsavebox{\unassigncircuit}
\savebox{\unassigncircuit}{
\begin{quantikz}
    \lstick{$\ket{\ensuremath{R}}$} & \gate[wires=2]{U_{\ensuremath{e}}^\dagger}\qwbundle[alternate]{} & \rstick{$\ket{\ensuremath{R}}$} \qwbundle[alternate]{} \\
    \lstick{$\ket{x}$} & \qwbundle{\hspace{-1em}k} & \rstick{$\ket{0}^{\otimes k}$} \qwbundle{k}\end{quantikz}
}
\newsavebox{\seqcircuit}
\savebox{\seqcircuit}{
\begin{quantikz}
    \lstick{$\ket{\ensuremath{R}, \ensuremath{M}}$} & \gate{\circuit{\ensuremath{s}_1}}\qwbundle[alternate]{} & \gate{\circuit{\ensuremath{s}_2}}\qwbundle[alternate]{} & \rstick{$\ket{\ensuremath{R}', \ensuremath{M}'}$} \qwbundle[alternate]{}
\end{quantikz}
}
\newsavebox{\swapcircuit}
\savebox{\swapcircuit}{
\begin{quantikz}
    \lstick{$\ket{x_1}$} & \swap{1}\qwbundle{\hspace{-1em}k} & \rstick{$\ket{x_1}$} \qwbundle{k} \\
    \lstick{$\ket{x_2}$} & \targX{}\qwbundle{\hspace{-1em}k} & \rstick{$\ket{x_2}$} \qwbundle{k}
\end{quantikz}
}
\newsavebox{\memswapcircuit}
\savebox{\memswapcircuit}{
\begin{quantikz}
    \lstick{$\ket{x_1}$} & \gate[wires=3]{\textrm{qRAM}}\qwbundle{\hspace{-1em}k_1} & \rstick{$\ket{x_1}$} \qwbundle{k_1} \\
    \lstick{$\ket{x_2}$} & \qwbundle{\hspace{-1em}k_2} & \rstick{$\ket{x'_2}$} \qwbundle{k_2} \\
    \lstick{$\ket{\ensuremath{M}}$} & \qwbundle[alternate]{} & \rstick{$\ket{\ensuremath{M}'}$} \qwbundle[alternate]{}
\end{quantikz}
}
\newsavebox{\ifcircuit}
\savebox{\ifcircuit}{
\begin{quantikz}
    \lstick{$\ket{x}$} & \ctrl{1} & \rstick{$\ket{x}$} \qw \\
    \lstick{$\ket{\ensuremath{R}, \ensuremath{M}}$} & \gate{\circuit{s}}\qwbundle[alternate]{} & \rstick{$\ket{\ensuremath{R}', \ensuremath{M}'}$} \qwbundle[alternate]{}
\end{quantikz}
}
\begin{figure}
\captionsetup[subfigure]{labelformat=empty}
\captionsetup{justification=centering}
\centering
\begin{subfigure}[b]{.3\textwidth}
\centering
\makebox(100,20){\usebox{\skipcircuit}}
\caption{$\circuit{\ensuremath{\texttt{skip}}}$ \\ (identity circuit)}
\end{subfigure}
\begin{subfigure}[b]{.6\textwidth}
\centering
\makebox(100,20){\usebox{\seqcircuit}}
\caption{$\circuit{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}$ \\ (concatenation)}
\end{subfigure}
\begin{subfigure}[b]{.4\textwidth}
\centering
\makebox(100,60){\usebox{\assigncircuit}}
\caption{$\circuit{\sBind{x}{\ensuremath{e}}}$ \\ (execute oracle)}
\end{subfigure}
\begin{subfigure}[b]{.4\textwidth}
\centering
\makebox(100,60){\usebox{\unassigncircuit}}
\caption{$\circuit{\sUnbind{x}{\ensuremath{e}}}$ \\ (un-execute oracle)}
\end{subfigure}
\begin{subfigure}[b]{.3\textwidth}
\centering
\makebox(100,75){\usebox{\swapcircuit}}
\caption{$\circuit{\sSwap{x_1}{x_2}}$ \\ (swap)}
\end{subfigure}
\begin{subfigure}[b]{.3\textwidth}
\centering
\makebox(100,75){\usebox{\memswapcircuit}}
\caption{$\circuit{\sMemSwap{x_1}{x_2}}$ \\ (random access)}
\end{subfigure}
\begin{subfigure}[b]{.3\textwidth}
\centering
\makebox(100,75){\usebox{\ifcircuit}}
\caption{$\circuit{\sIf{x}{s}}$ \\ (conditional gate)}
\end{subfigure}
\caption{Definition of quantum circuit semantics of Core \LangName{}{}.} \label{fig:core-circuit}
\end{figure}

In~\Cref{fig:core-circuit}, we translate a Core \LangName{}{} statement $\ensuremath{s}$ to a circuit fragment $\circuit{\ensuremath{s}}$ operating on the register file $\ensuremath{R}$ and memory $\ensuremath{M}$ encoded as quantum states. In the circuits, a wire depicted as \smash{\hspace{-0.6em}\raisebox{0.3em}{$\oset{\hspace{1.7em}\tiny k}{\usebox{\slashwire}}$}\hspace{-0.1em}}{} denotes a $k$-bit register representing an individual program value. A wire depicted as \hspace{-0.6em}\raisebox{0.3em}{\usebox{\tripwire}}\hspace{-0.1em}{} denotes a collection of such values, such as $\ensuremath{R}$ and $\ensuremath{M}$. A circuit fragment may be expanded to operate on the entire program state by tensor product with the identity gate.

The $\ensuremath{\texttt{skip}}$ statement translates to the identity circuit that maps a quantum state containing $\ensuremath{R}$ and $\ensuremath{M}$ to itself. Statements $\ensuremath{s}_1$ and $\ensuremath{s}_2$ are sequenced by concatenating their corresponding circuits $\circuit{\ensuremath{s}_1}$ and $\circuit{\ensuremath{s}_2}$. An expression $\ensuremath{e}$ is assigned to $x$ by initializing a zero register, executing $U_\ensuremath{e}$ on $\ket{R}$ and this register, and naming the resulting register $x$. An expression is un-assigned by executing $U_\ensuremath{e}^\dagger$, the inverse of $U_\ensuremath{e}$, producing a register of zeroes that is discarded from the circuit. Variables $x_1$ and $x_2$ are swapped using swap gates across their entire bit register representations. A swap with memory is performed by invoking the quantum random access gate (\Cref{sec:background}) on the address $x_1$, value $x_2$, and memory $\ensuremath{M}$. For an \texttt{if}-statement, its body $\circuit{\ensuremath{s}}$ is executed, conditioned on the bit $x$.

\paragraph{Soundness}
The circuit semantics defines a unitary operator $\circuit{\ensuremath{s}} : \ket{\ensuremath{R}, \ensuremath{M}} \mapsto \ket{\ensuremath{R}', \ensuremath{M}'}$ for each statement $\ensuremath{s}$. It faithfully represents the operational semantics of the statement in Core \LangName{}{}:
\begin{theorem}[Semantics Equivalence]
    $\circuit{\ensuremath{s}}\ket{\ensuremath{R}, \ensuremath{M}} = \ket{\ensuremath{R}', \ensuremath{M}'}$ iff $\sstepstar{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}'}{\ensuremath{M}'}$
\end{theorem}

\begin{proof}
    By induction on the structure of $\ensuremath{s}$.
\end{proof}

\section{Data Structure Descriptions} \label{sec:data-structure-descriptions}

In this section, we describe in detail the data structures we implemented and notable differences from their classical equivalents in usage or development process.

\paragraph{Linked List}

We implemented four operations that recursively traverse linked lists:
\begin{itemize}
    \item $\texttt{length}(\texttt{l})$ returns the length of \texttt{l} in $O(n)$ time.
    \item $\texttt{sum}(\texttt{l})$ returns the sum of elements in \texttt{l} in $O(n)$ time.
    \item $\texttt{find\_pos}(\texttt{l}, \texttt{x})$ returns the position of \texttt{x} in \texttt{l} in $O(n)$ time.
    \item $\texttt{remove}(\texttt{l}, \texttt{x})$ removes \texttt{x} from \texttt{l} and returns its position in $O(n)$ time.
\end{itemize}

Implementing these operations reversibly in linear time required overcoming the challenges of recursive uncomputation and mutated uncomputation.

\paragraph{Stack and Queue}

These operations manipulate a linked list as a LIFO stack and a FIFO queue:
\begin{itemize}
    \item $\texttt{push\_front}(\texttt{l}, \texttt{x})$ pushes \texttt{x} to the front of \texttt{l} in $O(1)$ time.
    \item $\texttt{pop\_front}(\texttt{x})$ pops an element from the front of \texttt{l} and returns it in $O(1)$ time.
    \item $\texttt{push\_back}(\texttt{l}, \texttt{x})$ pushes \texttt{x} to the back of \texttt{l} in $O(n)$ time.
\end{itemize}

The time complexity of \texttt{push\_back} is linear because we use a singly-linked list and could be further improved using a doubly-linked list.

\paragraph{String}

We implemented strings using two underlying representations: variable-length character arrays, which are not history-independent,\footnotemark{} and fixed-length words, which are. Only the word implementation is summarized in~\Cref{tbl:results}. The following operations are common to both implementations:
\footnotetext{We do not consider these arrays to be history-independent as they consist of a contiguous variable-length block rather than linked nodes that can be allocated from a pool of fixed-size blocks.}
\begin{itemize}
    \item $\texttt{is\_empty}(\texttt{s})$ returns whether \texttt{s} is an empty string in $O(1)$ time.
    \item $\texttt{length}(\texttt{s})$ returns the length of \texttt{s} in $O(1)$ time.
    \item $\texttt{get\_prefix}(\texttt{s}, \texttt{i})$ returns the prefix substring of length \texttt{i} of \texttt{s}.
    \item $\texttt{get\_substring}(\texttt{s}, \texttt{i})$ returns the suffix substring beginning at index \texttt{i} of \texttt{s}.
    \item $\texttt{get}(\texttt{s}, \texttt{i})$ returns character \texttt{i} of \texttt{s}.
    \item $\texttt{is\_prefix}(\texttt{s1}, \texttt{s2})$ returns whether \texttt{s1} is a prefix of \texttt{s2}.
    \item $\texttt{num\_matching}(\texttt{s1}, \texttt{s2})$ returns the number of characters that match in \texttt{s1} and \texttt{s2} starting from the beginning of both strings.
    \item $\texttt{equal}(\texttt{s1}, \texttt{s2})$ returns whether \texttt{s1} and \texttt{s2} are equal strings.
\end{itemize}

The time complexities of \texttt{get\_prefix}, \texttt{get\_substring}, and \texttt{get} are $O(1)$ for array-based strings, which use pointer arithmetic, and $O(k)$ for word-based strings, which use bitwise operations whose complexity increases with the word size. The complexities of \texttt{is\_prefix} and \texttt{num\_matching} are $O(n)$ for arrays and $O(\textrm{poly}(k))$ for words, which both use recursion. The complexity of \texttt{equal} is $O(n)$ for arrays, which use recursion, and $O(k)$ for words, which uses bitwise comparison.

The following operations are implemented for word-based strings only:
\begin{itemize}
    \item $\texttt{concat}(\texttt{s1}, \texttt{s2})$ returns the concatenation of \texttt{s1} and \texttt{s2} in $O(\textrm{poly}(k))$ time.
    \item $\texttt{compare}(\texttt{s1}, \texttt{s2})$ returns whether $\texttt{s1} \le \texttt{s2}$ lexicographically in $O(\textrm{poly}(k))$ time.
\end{itemize}

\paragraph{Set}

We implement the abstract data structure of sets using radix trees~\citep{morrison}. Unlike hash tables, radix trees are history-independent, and for any set of keys there exists a unique radix tree encoding the set. The set supports the interface:
\begin{itemize}
    \item $\texttt{insert}(\texttt{s}, \texttt{k}, \texttt{v})$ inserts key $\texttt{k}$ into set $\texttt{s}$ in $O(\textrm{poly}(k))$ time.
    \item $\texttt{contains}(\texttt{s}, \texttt{k})$ returns whether set $\texttt{s}$ contains key $\texttt{k}$ in $O(\textrm{poly}(k))$ time.
\end{itemize}

The radix tree structure was by far the most complex data structure to implement in the library, at over 400 lines of code in Tower{}. Implementing an efficient tree traversal required overcoming all three challenges, particularly branch sequentialization (\Cref{sec:branch-sequentialization}).

For comparison, we also implemented sets using separate-chaining hash tables, which are not history-independent. This interface is actually more general, supporting map operations that additionally associate a key with a value:
\begin{itemize}
    \item $\texttt{insert}(\texttt{m}, \texttt{k}, \texttt{v})$ inserts $\texttt{v}$ at $\texttt{k}$ into map $\texttt{m}$ and returns the old value if present, in $O(n)$ time.
    \item $\texttt{contains}(\texttt{m}, \texttt{k})$ returns whether map $\texttt{m}$ contains key $\texttt{k}$ in $O(n)$ time.
\end{itemize}

Classically, the complexity of hash table operations is $O(n)$ in the worst case of maximal hash collisions and has $O(1)$ average complexity. The quantum implementation always incurs the $O(n)$ worst case complexity in the general case with no guarantees on hash function performance.

One may invoke \texttt{insert} twice to copy a value out of the map for a given key.
Because \texttt{insert} is reversible, it is also possible to remove the elements of a hash table in the order they were inserted by reversing the \texttt{insert} operation:
\begin{lstlisting}[style=nonum]
let null <- insert[N](m, 1, 2);
let null <- insert[N](m, 2, 4);
let null -> insert[N](m, 2, 4); /* Must remove in this order */
let null -> insert[N](m, 1, 2);
\end{lstlisting}
However, removing elements in a different order may corrupt the state of the hash table, because a separate-chaining hash table is not history-independent in general.

\section{Implementation}

We implemented an interpreter for Tower{} in OCaml that classically executes the operational semantics of the language. The type checker ensures that a program uses bounded recursion and contains code uncomputing each temporary value, and the interpreter verifies at runtime that 1) values are uncomputed correctly and 2) all heap memory is freed by the end of the program.

We also implemented a compiler for Tower{} into quantum circuits. Given a Tower{} program, the compiler generates for each function a reversible logic circuit that when executed on a bit-representation of its input stores its output into an auxiliary register. The compiler outputs assembly code that invokes primitive logical, arithmetic, and memory operations.

Furthermore, the compiler can instantiate these operations with reversible logic, arithmetic, and qRAM gates built from multi-controlled-NOT gates. The current implementations of these operations prioritize simplicity; more optimized designs from the literature are possible but not currently implemented. The output is in a simple textual netlist format that is amenable to conversion for use in available quantum computation frameworks.

\section{Ground{}: Data Structure Library and Challenges} \label{sec:data-structure-library}

We implemented Ground{}, a library of abstract data structures in Tower{}, and tested its operations with the interpreter and compiler. We also encountered several challenges during the development process that do not arise in classical programming, and share them with future quantum developers.

\subsection{Summary of Data Structure Library}

\Cref{tbl:results} summarizes the Ground{} data structure library. We implemented the abstract data structures of lists, stacks, queues, strings, and sets.\footnotemark{} In the table, the name of an an abstract data structure is followed by its underlying implementation in parentheses. All implementations are history-independent except for hash table-based sets.
\footnotetext{Maps may be implemented as a straightforward augmentation of sets with values stored alongside each key.}

The time complexity for certain pointer-based data structures is a function of $n$, the number of elements in the data structure. For word-based data structures, the complexity of operations instead scales with the system word size $k$,\footnotemark{} and becomes polynomial in $k$ if the operation performs recursion bounded by $k$ and performs operations over words of size $k$ at each level.
\footnotetext{The word size $k$ is in turn logarithmic in the maximum number of elements $n$ of the data structure.}

We report the counts of qubits and gates used by the compiled circuit for each operation, including temporary qubits, after minimal optimization. To focus on the fundamental complexity of each operation, these counts exclude 1) the qubits constituting the qRAM, 2) qubits and gates internal to the implementation of primitive logical, arithmetic, and memory operations, and 3) gates to copy and swap qubits, all of which are highly dependent on parameter and optimization choices. For operations with variable complexity, these counts are functions of $n$ or $k$. Word sizes $4 \le k \le 12$ are assumed for operations whose complexity depends on $k$, and $k = 8$ is assumed otherwise.

In~\Cref{sec:data-structure-descriptions}, we detail the characteristics of each data structure.
In the following sections, we describe three challenges of implementing data structure operations as quantum programs: recursive uncomputation, mutated uncomputation, and branch sequentialization.

\newcommand{\textcolor{gray}{$-$}}{\textcolor{gray}{$-$}}
\begin{table}
\caption{Overview of Ground{} library. All operations are reversible. ``Recursion''  denotes whether the operation uses bounded recursion. ``Mutation'' indicates whether it leaves input in a mutated state. ``Complexity'' indicates its time complexity in terms of the number of elements $n$ or the word size $k$. ``LoC'' counts the lines of code implementing the operation and its dedicated helpers, excluding calls to other operations listed here. ``Qubits'' counts qubits used, excluding those internal to the qRAM and primitive logic/arithmetic/memory operations. ``Gates'' counts primitive logic/arithmetic/memory gates invoked, excluding copy/swap gates.}
\begin{threeparttable}
\resizebox{\textwidth}{!}{%
\begin{tabular}{ l c c c c c c c }
\toprule
Data Structure                      & Reversible & Recursion & Mutation & Complexity & LoC & Qubits & Gates \\
\midrule
List & & & \\
\textcolor{gray}{$-$}{} \texttt{length}          & Yes & Yes & No  & $O(n)$ & 20 & $34n + 32$ & $23n + 3$ \\
\textcolor{gray}{$-$}{} \texttt{sum}             & Yes & Yes & No  & $O(n)$ & 20 & $34n + 40$ & $21n + 3$ \\
\textcolor{gray}{$-$}{} \texttt{find\_pos}       & Yes & Yes & No  & $O(n)$ & 20 & $42n + 31$ & $19n + 3$ \\
\textcolor{gray}{$-$}{} \texttt{remove}          & Yes & Yes & Yes & $O(n)$ & 48 & $26n + 56$ & $42n + 3$ \\
Stack (list) & & & \\
\textcolor{gray}{$-$}{} \texttt{push\_front}     & Yes & No  & Yes & $O(1)$ & 8 & 40 & 4 \\
\textcolor{gray}{$-$}{} \texttt{pop\_front}      & Yes & No  & Yes & $O(1)$ & 8 & 48 & 4 \\
Queue (list) & & & \\
\textcolor{gray}{$-$}{} \texttt{push\_back}      & Yes & Yes & Yes & $O(n)$ & 21 & $34n + 32$ & $24n$ \\
\textcolor{gray}{$-$}{} \texttt{pop\_front}      & Yes & No  & Yes & $O(1)$ & 8 & 48 & 4 \\
String (word) & & & \\
\textcolor{gray}{$-$}{} \texttt{is\_empty}       & Yes & No  & No  & $O(1)$ & 2 & 25 & 3 \\
\textcolor{gray}{$-$}{} \texttt{length}          & Yes & No  & No  & $O(1)$ & 2 & 24 & 1 \\
\textcolor{gray}{$-$}{} \texttt{get\_prefix}     & Yes & No  & No  & $O(k)$ & 8 & $11k$ & 52 \\
\textcolor{gray}{$-$}{} \texttt{get\_substring}  & Yes & No  & No  & $O(k)$ & 8 & $12k$ & 54 \\
\textcolor{gray}{$-$}{} \texttt{get}             & Yes & No  & No  & $O(k)$ & 7 & $6k + 1$ & 19 \\
\textcolor{gray}{$-$}{} \texttt{is\_prefix}      & Yes & Yes & No  & $O(\textrm{poly}(k))$ & 26 & $k^2 + 11k$ & $98k + 3$ \\
\textcolor{gray}{$-$}{} \texttt{num\_matching}   & Yes & Yes & No  & $O(\textrm{poly}(k))$ & 42 & $k^2 + 13k + 4$ & $110k + 127$ \\
\textcolor{gray}{$-$}{} \texttt{equal}           & Yes & No  & No  & $O(k)$ & 8 & $6k + 3$ & 5 \\
\textcolor{gray}{$-$}{} \texttt{concat}          & Yes & No  & No  & $O(k)$ & 9 & $11k$ & 8 \\
\textcolor{gray}{$-$}{} \texttt{compare}         & Yes & Yes & No  & $O(\textrm{poly}(k))$ & 27 & $5k^2 + 12k$ & $108k + 3$ \\
Set (radix tree) & & & \\
\textcolor{gray}{$-$}{} \texttt{insert}          & Yes & Yes & Yes & $O(\textrm{poly}(k))$ & 136 & $13k^2 + 21k + 9$ & $1440k^2 + 5056k$ \\
\textcolor{gray}{$-$}{} \texttt{contains}        & Yes & Yes & No  & $O(\textrm{poly}(k))$ & 334 & $17k^2 + 18k + 2$ & $784k^2 + 1612k + 1$ \\
Set (hash table)${}^\ast$ & & & \\
\textcolor{gray}{$-$}{} \texttt{insert}          & Yes & Yes & Yes & $O(n)$ & 63 & $52n + 72$ & $68n + 15$ \\
\textcolor{gray}{$-$}{} \texttt{contains}        & Yes & Yes & No  & $O(n)$ & 7 & $52n + 81$ & $136n + 39$ \\
\bottomrule
\end{tabular}%
}
\begin{tablenotes}
\footnotesize\sffamily
\item${}^\ast$ Hash table-based sets are not history-independent.
\end{tablenotes}
\end{threeparttable}
\label{tbl:results}
\end{table}

\subsection{Challenge 1: Recursive Uncomputation} \label{sec:recursive-uncomputation}

\emph{Recursive uncomputation} arises when the result of a recursive call is uncomputed, and causes certain functions to incur exponential slowdown in asymptotic time complexity. We must be careful to appropriately craft the implementation to avoid naive implementations that cause this slowdown.

\begin{figure}
\centering
\begin{minipage}[t]{.45\textwidth}
\begin{lstlisting}[label={lst:length-exponential}]
fun length[n](l: ptr<list>) -> uint {
  with {
    let l_empty <- l == null;
  } do if l_empty {
    let out <- 0;
  } else with {
    let temp <- default<list>;
    *l <-> temp;
    let next <- temp.2;
    let r <- length[n-1](next);
  } do {
    let out <- r + 1;
  }
  return out;
}
\end{lstlisting}
\end{minipage}%
\begin{minipage}[t]{.55\textwidth}
\begin{lstlisting}[label={lst:length-linear}]
fun length[n](l: ptr<list>, acc: uint) -> uint {
  with {
    let l_empty <- l == null;
  } do if l_empty {
    let out <- acc;
  } else with {
    let temp <- default<list>;
    *l <-> temp;
    let next <- temp.2;
    let r <- acc + 1;
  } do {
    let out <- length[n-1](next, r);
  }
  return out;
}
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{.45\textwidth}
\caption{$O(2^n)$-time list \lstinline{length}.} \label{fig:length-exponential}
\end{minipage}%
\begin{minipage}[t]{.55\textwidth}
\caption{$O(n)$-time, avoiding recursive uncomputation.} \label{fig:length-linear}
\end{minipage}
\end{figure}
In~\Cref{fig:length-exponential}, we present a correct but inefficient way to compute the length of a linked list.
Line~\ref{lst:length-exponential-3} determines if the list \lstinline{l} is empty. If so, line~\ref{lst:length-exponential-5} sets the output to zero, and if not, lines~\ref{lst:length-exponential-7}--\ref{lst:length-exponential-9} obtain a pointer \lstinline{next} to the tail of the list. Line~\ref{lst:length-exponential-10} recursively computes the length of the tail. Line~\ref{lst:length-exponential-12} adds one to the result of the recursion. After the \lstinline{do}-block completes, Tower{} reverses the effects of both prior \lstinline{with}-blocks to uncompute all temporary variables and restore the original state of the list.

\paragraph{Recursive Uncomputation}

Though the program in~\Cref{fig:length-exponential} is correct, its time complexity is $O(2^n)$. The reason is that the recursive call on line~\ref{lst:length-exponential-10} produces a temporary value \lstinline{r} that is uncomputed at the end of the \lstinline{do}-block. As a result, \lstinline{length} makes both a forward and a reverse recursive call at each level, resulting in exponential complexity.

Avoiding recursive uncomputation requires not uncomputing the result of recursive calls. One possible approach is inspired by tail recursion from classical programming, where the result of a recursive call is returned without any intervening operations.

In~\Cref{fig:length-linear}, we avoid recursive uncomputation with an extra accumulator argument. Line~\ref{lst:length-linear-5} returns the accumulator in the base case. Line~\ref{lst:length-linear-10} adds one to the accumulator, and line~\ref{lst:length-linear-12} recursively calls the function with the new accumulator and directly assigns the result to the output.

Calling this function with an initial accumulator of zero returns the length. In the new implementation, no second recursive call is necessary, and the implementation achieves $O(n)$ complexity.

We encountered this challenge in the implementations of \lstinline{find_pos}, \lstinline{length}, \lstinline{remove}, and \lstinline{sum} for lists as well as \lstinline{is_prefix}, \lstinline{num_matching}, and \lstinline{compare} for strings.

\subsection{Challenge 2: Mutated Uncomputation} \label{sec:mutated-uncomputation}

\emph{Mutated uncomputation} refers to when uncomputing a temporary value is not straightforward because the program mutates data under conditional branches. The typical strategy of uncomputing a temporary using the expression that originally computed it fails when variables in that expression have been mutated by intervening statements.

In~\Cref{fig:push-back}, we implement the \lstinline{push_back} operation, which adds \lstinline{x} to the end of \lstinline{l}. Line~\ref{lst:push-back-2} computes the flag \lstinline{l_empty}. If it is true, lines~\ref{lst:push-back-4}--\ref{lst:push-back-7} allocate a new node storing \lstinline{x} and set \lstinline{l} to point to it. Otherwise, line~\ref{lst:push-back-12} extracts the \lstinline{tail} of the list, and line~\ref{lst:push-back-15} recursively calls \lstinline{push_back} on it.

\begin{wrapfigure}[24]{r}{.46\textwidth}
\vspace*{-1.5em}
\begin{lstlisting}[label={lst:push-back}]
fun push_back[n](l: ptr<list>, x: uint) {
  let l_empty <- l == null;
  if l_empty {
    let head <- alloc<list>;
    l <-> head;
    let head -> null;
    let node <- (x, null);
  } else {
    let node <- default<list>;
    *l <-> node;
    with {
      let (h, tail) <- node;
      let node -> (h, tail);
    } do {
      let () <- push_back[n-1](tail, x);
    }
  }
  let l_empty -> node.2 == null;
  *l <-> node;
  let node -> default<list>;
  return ();
}
\end{lstlisting}
\caption{Implementation of \lstinline{push_back}.} \label{fig:push-back}
\end{wrapfigure}

\paragraph{Mutated Uncomputation}
Line~\ref{lst:push-back-18} uncomputes \lstinline{l_empty} differently from its computation on line~\ref{lst:push-back-2}. The reason is that \lstinline{l} may have been modified by line~\ref{lst:push-back-5}, which would break the relationship between \lstinline{l} and \lstinline{l_empty}. Instead, the program uncomputes \lstinline{l_empty} based on whether the tail of the new list stored in \lstinline{node} is \lstinline{null} on line~\ref{lst:push-back-18}, which is true if and only if \lstinline{l_empty} was true after line~\ref{lst:push-back-2}.

Thus, correctly uncomputing certain values requires reasoning about the data structure invariants that hold on the state after mutation.
We encountered this challenge in \lstinline{remove} for lists, \lstinline{push_back} for queues, and \lstinline{insert} for sets implemented using both hash tables and radix trees.
By contrast, operations that do not mutate data usually can uncompute temporaries straightforwardly.

\subsection{Challenge 3: Branch Sequentialization} \label{sec:branch-sequentialization}
\begin{figure}
\centering
\vspace*{-0.5em}
\begin{minipage}[t]{.48\textwidth}
\begin{lstlisting}[label={lst:contains-linear}]
fun contains(t: tree, k: uint) -> bool {
  if t == null { let out <- false; }
  else if t.1 == k { let out <- true; }
  else if t.1 < k {
    let out <- contains(t.2, k);
  } else {
    let out <- contains(t.3, k);
  }
  return out;
}
\end{lstlisting}
\end{minipage}%
\begin{minipage}[t]{.52\textwidth}
\begin{lstlisting}[label={lst:contains-log}]
fun contains(t: tree, k: uint) -> bool {
  if t == null { let out <- false; }
  else if t.1 == k { let out <- true; }
  else {
    if t.1 < k { let child <- t.2; }
    else { let child <- t.3; }
    let out <- contains(child, k);
  }
  return out;
}
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{.45\textwidth}
\caption{$O(n)$-time binary tree traversal.} \label{fig:contains-linear}
\end{minipage}%
\begin{minipage}[t]{.55\textwidth}
\caption{$O(\log n)$-time, avoiding branch sequentialization.} \label{fig:contains-log}
\end{minipage}
\end{figure}
\emph{Branch sequentialization} refers to the fact that the time complexity of a conditionally branching quantum program is often larger than its classical equivalent and the developer may need to structure the program differently to avoid slowdown.

In~\Cref{fig:contains-linear}, we present a pseudo-Tower{} program that traverses a binary search tree. Classically, if \lstinline{t} is balanced, then the time complexity of the program is $O(\log n)$.

\paragraph{Branch Sequentialization}

However, if \Cref{fig:contains-linear} is compiled to a quantum circuit (\Cref{sec:circuit-semantics}), each \lstinline{if}-statement becomes a gate that conditions over the gate translation of the \lstinline{if}-body. Each recursive level of the resulting circuit contains a gate that traverses the left child and a gate that traverses the right child, resulting in $O(n)$ total complexity. Put simply, the time complexity of a quantum program is the sum and not the maximum of the complexities of its possible branches.

Efficiently traversing a branching data structure requires making only one recursive call in the function. In~\Cref{fig:contains-log}, we present a program that performs such a traversal in $O(\log n)$.

We encountered this challenge in radix tree \lstinline{insert} and \lstinline{contains}, which use a similar approach to attain poly-logarithmic complexity in the number of elements.

\section{Quantum Data Structures in Tower{}} \label{sec:examples}

In this section, we present data structures in quantum superposition and the properties of reversibility, history independence, and bounded-time execution. We illustrate how a developer uses Tower{} to implement fundamental data structures satisfying these properties.

\subsection{Linked Data in Superposition}

In classical computing, linked data forms the basis of numerous abstract data structures. For example, linked lists may concretely implement abstract stacks, queues, and sets.
We use the notation \pstate{\texttt{l} \ensuremath{\hookrightarrow} [1,2]} to represent a classical program state\footnotemark{} in which the variable \lstinline{l} denotes a linked list storing the integers 1 and 2.
\footnotetext{A classical program state is a bit string, meaning that the set of all program states is finite.}

\paragraph{Superposition}

In a Tower{} program, the state of all program variables and memory exists in quantum superposition. For example, the quantum state of the program may be in a uniform superposition of three classical states in which \lstinline{l} denotes different linked lists:
\[
    \frac{1}{\sqrt{3}}\left(\ket{\pstate{\texttt{l} \ensuremath{\hookrightarrow} []}} + \ket{\pstate{\texttt{l} \ensuremath{\hookrightarrow} [1,2]}} + \ket{\pstate{\texttt{l} \ensuremath{\hookrightarrow} [1,\ldots,100]}}\right)
\]

\paragraph{Data Structure Operations}
We may lift a classical operation on a list to a unitary operation on a list in superposition. For example, the stack operation \lstinline{push_front} prepends an element onto every list in the superposition. Executing $\texttt{push\_front}(\texttt{l}, 6)$ would produce a new quantum state:
\[
    \frac{1}{\sqrt{3}}\left(\ket{\pstate{\texttt{l} \ensuremath{\hookrightarrow} [6]}} + \ket{\pstate{\texttt{l} \ensuremath{\hookrightarrow} [6,1,2]}} + \ket{\pstate{\texttt{l} \ensuremath{\hookrightarrow} [6,1,\ldots,100]}}\right)
\]

\paragraph{Memory Representation}

\newcommand{\,\raisebox{-0.1em}{\scalebox{0.8}{\begin{tikzpicture}{\,\raisebox{-0.1em}{\scalebox{0.8}{\begin{tikzpicture}
\draw (2.4, 0.6) rectangle (2.8, 1);
\draw (2.4, 0.6) -- (2.8, 1);
\end{tikzpicture}}}\,}

The memory representation of a singly-linked list is a collection of nodes, each consisting of content data and a pointer to the next node, or \lstinline{null} if there is none.

Within a classical program state, \lstinline{null} denotes the empty list, and a pointer to a memory location at which a pair of 1 and \lstinline{null} are stored denotes the singleton list containing the element 1. The program state $\pstate{\texttt{l} \ensuremath{\hookrightarrow} [1,2]}$ is depicted by the following diagram, in which \,\raisebox{-0.1em}{\scalebox{0.8}{\begin{tikzpicture{} denotes \lstinline{null}:
\vspace{0.5em}
\begin{center}
\begin{tikzpicture}
\node at (-0.3, 0.8) {\texttt{l}};
\draw (0, 0.6) rectangle (0.4, 1);
\draw[black,fill=black] (0.2, 0.8) circle (.4ex);
\draw[-stealth, thick] (0.2, 0.8) -- (0.7, 0.8);

\draw (0.8, 0.6) rectangle (1.2, 1);
\draw (1.2, 0.6) rectangle (1.6, 1);
\node at (1, 0.8) {1};
\draw[black,fill=black] (1.4, 0.8) circle (.4ex);
\draw[-stealth, thick] (1.4, 0.8) -- (1.9, 0.8);

\draw (2, 0.6) rectangle (2.4, 1);
\draw (2.4, 0.6) rectangle (2.8, 1);
\node at (2.2, 0.8) {2};
\draw (2.4, 0.6) -- (2.8, 1);
\end{tikzpicture}
\end{center}
\subsection{Implementation with Tower{}}

Tower{} makes it possible to implement linked data structures in quantum superposition. A key aspect of its design is a set of programming primitives that are each \emph{reversible}, meaning it can be executed forwards or backwards to produce or reverse its computational effect. For example, a program may execute $\texttt{push\_front}(\texttt{l}, 6)$ forwards, updating the state of \lstinline{l} by prepending 6. The program may also execute the function backwards by removing 6 from the front of \lstinline{l}.

\paragraph{Reversibility}

Reversible primitives correspond to unitary operators that can be realized as gates in a quantum computer (\Cref{sec:background}). Though a quantum computer is also capable of performing irreversible measurement, measurement collapses the program state from superposition into a classical state, which causes algorithms such as~\citet{ambainis2003,aaronson2019,bernstein2013} to produce incorrect outputs or lose their efficiency advantage. Thus, we designed Tower{} with reversible operators that make it possible to implement data structures correctly.

\begin{figure}[b]
\centering
\vspace*{-.5em}
\begin{minipage}[t]{.5\textwidth}
\begin{lstlisting}[label={lst:push-front}]
fun push_front(l: ptr<list>, x: uint) {
  let head <- alloc<list>;
  l <-> head;                /* Swap */
  let node <- (x, head);
  let head -> node.2;        /* Uncompute */
  *l <-> node;               /* Swap */
  let node -> default<list>; /* Uncompute */
  return ();
}
\end{lstlisting}
\end{minipage}%
\begin{minipage}[t]{.5\textwidth}
\begin{lstlisting}[label={lst:push-back}]
fun pop_front(l: ptr<list>) -> uint {
  let node <- default<list>;
  *l <-> node;
  let head <- node.2;
  let x <- node.1;  /* Get output */
  let node -> (x, head);
  l <-> head;
  let head -> alloc<list>;
  return x;
}
\end{lstlisting}
\end{minipage}

\setlength{\abovecaptionskip}{0pt}
\setlength{\belowcaptionskip}{-5pt}
\begin{minipage}[b]{0.5\textwidth}
\captionof{figure}{Implementation of \lstinline{push_front}.} \label{fig:push-front}
\end{minipage}%
\begin{minipage}[b]{0.5\textwidth}
\captionof{figure}{Implementation of \lstinline{pop_front}.} \label{fig:pop-front}
\end{minipage}
\end{figure}

\paragraph{Implementing \texttt{push\_front}}

In Tower{}, the type of linked lists of integers is:
\begin{lstlisting}[style=nonum]
type list = (uint, ptr<list>);
\end{lstlisting}
In~\Cref{fig:push-front}, we implement $\texttt{push\_front}(\texttt{l},\texttt{x})$, and in~\Cref{fig:push-steps} we depict the effect of each line diagrammatically. At a high level, the function initializes a new list node \lstinline{head} that stores \lstinline{x} and points to \lstinline{l} as its next node. Then, it writes \lstinline{head} in place of the input \lstinline{l} and returns.

\subfile{execution}

In~\Cref{fig:push-step-1}, we depict the initial program state of $\texttt{push\_front}(\texttt{l},6)$, assuming \lstinline{l} denotes $[1,2]$. \Cref{fig:push-step-2} depicts the effect of line~\ref{lst:push-front-2}, which uses the \lstinline{alloc} operator to allocate a new list node in memory named \lstinline{head}. Line~\ref{lst:push-front-3} (\Cref{fig:push-step-3}) uses the \emph{swap} operator \lstinline{<->} to swap the value of \lstinline{head} with the value of \lstinline{l}. Line~\ref{lst:push-front-4} (\Cref{fig:push-step-4}) assigns \lstinline{node} to be a pair of the input \lstinline{x} and \lstinline{head}.

\paragraph{Uncomputation}
Line~\ref{lst:push-front-5} (\Cref{fig:push-step-5}) \emph{un-assigns} \lstinline{head} from the second field of \lstinline{node}, meaning that it \emph{uncomputes} the value of the temporary variable \lstinline{head} and discards it.
Uncomputation~\citep{bennett1973} reverses the computation that produced a variable, restoring its value to zero.

We have designed Tower{} such that every program is reversible, meaning that the program cannot simply erase \lstinline{head} when it is no longer useful. If \lstinline{head} were erased with some unknown value, then an attempt to execute the program in reverse would be stuck, unable to materialize that value. Instead, the program must restore \lstinline{head} to a known constant before discarding it.
Specifically, the un-assignment on line~\ref{lst:push-front-5} is defined to be the reverse of the assignment:
\begin{lstlisting}[style=nonum]
let head <- node.2;
\end{lstlisting}
In Tower{}, this assignment would be implemented reversibly by initializing \lstinline{head} to all zeroes and flipping each bit conditioned on the corresponding bit of \lstinline{node.2}. Its reverse, the un-assignment on line~\ref{lst:push-front-5}, instead starts with \lstinline{head} equal to \lstinline{node.2}, and performs the same set of conditional bit flips. After these bit flips, the state of \lstinline{head} is reset to all zeroes, and the program discards it safely.

Continuing on, line~\ref{lst:push-front-6} (\Cref{fig:push-step-6}) swaps \lstinline{node} with memory at address \lstinline{l}. Because line~\ref{lst:push-front-3} swapped \lstinline{l} with an empty list node, after line~\ref{lst:push-front-6}, \lstinline{l} points to the list head and \lstinline{node} stores an empty node. Line~\ref{lst:push-front-7} (\Cref{fig:push-step-7}) then uncomputes \lstinline{node} as an empty node. Having updated the list \lstinline{l} and uncomputed all temporary values, the function then returns.

\paragraph{Reversing Operation}

In Tower{}, the syntactic reverse of $\texttt{push\_front}(\texttt{l}, \texttt{x})$ is also a meaningful program that removes \lstinline{x} from the front of \lstinline{l} instead of adding it. A familiar, closely related operation is \lstinline{pop_front}, the stack operation that removes the first element from a list and returns the element. Indeed, the implementation of \lstinline{pop_front} is nearly the syntactic reverse of \lstinline{push_front}.

In~\Cref{fig:pop-front}, we present \lstinline{pop_front}. It first reverses line~\ref{lst:push-front-7} of \lstinline{push_front}, replacing un-assignment with assignment, and then line~\ref{lst:push-front-6}, which remains identical --- the reverse of a swap operation is itself. It reverses line~\ref{lst:push-front-5} of \lstinline{push_front}, assigning the second field of \lstinline{node} to \lstinline{head}. Line~\ref{lst:push-front-5} of \lstinline{pop_front} is newly inserted --- it obtains \lstinline{x} from the first field of \lstinline{node} so that \lstinline{x} may be returned. The following lines reverse the first three lines of \lstinline{push_front}, and the function returns \lstinline{x}.

\subsection{Dynamic Memory Allocation with Boson{}}

Sets are foundational to programming and critical to algorithms. Surprisingly, many implementations of sets such as lists, hash tables, and binary trees are unsuitable for quantum programming.

\paragraph{Interference}

Algorithms such as~\citet{ambainis2003,aaronson2019,bernstein2013,buhrman2021} rely on \emph{interference}, or the constructive or destructive interaction of amplitudes in a quantum state.
For example,~\citet{ambainis2003} generates a superposition over program states $\pstate{\texttt{s} \ensuremath{\hookrightarrow} s_i}$, i.e. variable \texttt{s} denotes a set of integers $s_i$. The correctness of the algorithm relies on the fact that if $s_1$ and $s_2$ are sets containing the same integers, then their amplitudes interfere. In particular, suppose that $\gamma_1 = \gamma_2$ and $s_1 = \{1, 2\}$ and $s_2 = \{1, 2\}$. Then, the algorithm requires
\[
    \gamma_1 \ket{\pstate{\texttt{s} \ensuremath{\hookrightarrow} s_1}} - \gamma_2 \ket{\pstate{\texttt{s} \ensuremath{\hookrightarrow} s_2}} = 0.
\]

\paragraph{History Independence}

However, suppose that sets are implemented using linked lists, where $s_1$ is represented as $[1,2]$ and $s_2$ as $[2,1]$. Because $\pstate{\texttt{s} \ensuremath{\hookrightarrow} [1,2]}$ and $\pstate{\texttt{s} \ensuremath{\hookrightarrow} [2,1]}$ are physically distinct states, these terms do not cancel, causing the algorithm to produce incorrect outputs.

For the algorithm to execute correctly, the implementation of the data structure must satisfy \emph{history independence}.
We adapt its definition\footnotemark{} from \citet{teague2001}:
\footnotetext{This definition is termed the ``strong'' variant of history independence in the original work.}
\begin{definition}[History Independence]
    An abstract data structure implementation is \emph{history-independent} if and only if, when any two sequences of abstract operations yield semantically equivalent data structure instances, then the physical representations of the instances are identical.
\end{definition}

The implementation of a set as an unsorted linked list is not history-independent, as the lists $[1,2]$ and $[2,1]$ both represent the same set $\{1,2\}$.
Similarly, implementations of sets such as balanced binary trees or hash tables\footnotemark{} are not history-independent and are unsuitable for use in quantum algorithms that leverage interference.
\footnotetext{Other reasons why hash tables are unsuitable are 1) removal from a hash table is not directly reversible, and 2) all operations assume their worst case $O(n)$ rather than average case $O(1)$ complexity when all recursion is classically unfolded.}

\paragraph{Unique Linking Structure}

A history-independent implementation must assign each semantic instance of the data structure a unique linking structure in the underlying representation.
For example, suppose a set is instead implemented as a sorted list without duplicates. The set $\{1,2\}$ is then uniquely represented as the list $[1,2]$, ostensibly satisfying history independence.

\paragraph{Memory Addresses}

However, a unique linking structure does not by itself guarantee history independence.
In the example, the issue is that $\pstate{\texttt{s} \ensuremath{\hookrightarrow} [1,2]}$ may still refer to physically distinct program states in which the pointers to the linked list nodes take on different values.

\subfile{structures}

For example,~\Cref{fig:state-rep-1} depicts a program state in which \texttt{s} points to memory location 1, which stores value 1 and a pointer to memory location 3, which stores value 2 and \lstinline{null}. \Cref{fig:state-rep-2} depicts a state in which \texttt{s} points to memory location 5, which stores 1 and a pointer to memory location 1, which stores 2 and \lstinline{null}. These two program states are physically distinct but semantically equivalent, causing quantum interference to fail.

\paragraph{Boson{}}

We resolve this issue by developing Boson{}, a memory allocator that ensures that addresses of all dynamic allocations in the program are history-independent.
Under Boson{}, the single unique program state in which \texttt{s} denotes $[1,2]$ is~\Cref{fig:state-rep-3}, in which the linked list nodes are stored in a uniform superposition of all possible allocation sites.

\paragraph{Radix Trees}

The sorted list implementation of sets has $O(n)$ operation complexity, which is asymptotically inefficient.
By contrast, \citet{bernstein2013} propose using a radix tree~\citep{morrison}, whose linking structure is in one-to-one correspondence with sets and which supports operations in $O(\log n)$ time.
In this work, we construct an efficient and history-independent implementation of sets by combining the radix tree with the Boson{} dynamic memory allocator.

\subsection{Inductive Data Types in Tower{}}

The last tool needed to implement operations on linked data structures is recursion. We demonstrate recursion in Tower{} by implementing the function \lstinline{find_pos}, which returns the position of an integer \lstinline{x} in a list \lstinline{l}, assuming it is present in the list. This operation traverses to the end of the list, and a natural implementation performs this traversal recursively.

\paragraph{Recursion Bounds}

Classically, a recursive call pushes a return address onto the program stack and sets the program counter to the entry point of the function.
By contrast, a quantum processor does not possess a program counter or the ability to loop potentially infinitely.
All recursive procedures must instead be unrolled to a fixed, classically known depth, and inlined.

Tower{} guarantees that fully unrolling a recursive function is always possible using a classical \emph{recursion bound} specifying the number of recursion levels. The Tower{} type system verifies that in a program, all recursive function calls satisfy their respective recursion bound.

\paragraph{Implementing \texttt{find\_pos}}

In~\Cref{fig:find-pos}, we implement \lstinline{find_pos} in Tower{} by recursively traversing \lstinline{l} and comparing each element with \lstinline{x}.
The implementation takes an accumulator argument \lstinline{acc}, such that calling the function with zero for \lstinline{acc} returns the position of \lstinline{x}.

On line~\ref{lst:find-pos-1}, the bound \lstinline{[n]} denotes that \lstinline{find_pos} may recursively call itself at most \lstinline{n} times.
Lines~\ref{lst:find-pos-3}--\ref{lst:find-pos-13} feature a \lstinline{with}-\lstinline{do} statement, syntactic sugar that facilitates uncomputation. Tower{} executes this statement by executing the body of \lstinline{with}, then the \lstinline{do}, then the reverse of the \lstinline{with}. In this program, reversing the \lstinline{with}-block uncomputes \lstinline{node}, \lstinline{this_x}, \lstinline{next}, \lstinline{r}, and \lstinline{eq}.

Line~\ref{lst:find-pos-5} swaps the contents of memory at address \lstinline{l} with an empty node \lstinline{node}, and line~\ref{lst:find-pos-6} extracts from \lstinline{node} the content \lstinline{this_x} and pointer \lstinline{next} to the tail.
Line~\ref{lst:find-pos-8} computes \lstinline{eq}, a flag for whether \lstinline{this_x} is equal to \lstinline{x}. If it is, line~\ref{lst:find-pos-10} returns the current position, and if it is not, line~\ref{lst:find-pos-12} recursively calls \lstinline{find_pos} on the tail of the list, with a recursion bound that has decreased by one.

\section{Full Semantics} \label{sec:full-semantics}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[TV-Var]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}, x : \ensuremath{\tau}}{x}{\ensuremath{\tau}}}

\inferrule[TV-Unit]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\ensuremath{()}}{\ensuremath{()}}}

\inferrule[TV-Pair]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\tau}_2}}{\hastype{\ensuremath{\Gamma}}{\ePair{x_1}{x_2}}{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}}

\inferrule[TV-Num]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vNum{n}}{\ensuremath{\texttt{uint}}}}

\inferrule[TV-Bool]{b \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\hastype{\ensuremath{\Gamma}}{b}{\ensuremath{\texttt{bool}}}}

\inferrule[TV-Null]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vNull{\ensuremath{\tau}}}{\tPtr{\ensuremath{\tau}}}}

\inferrule[TV-Ptr]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vPtr{\ensuremath{\tau}}{p}}{\tPtr{\ensuremath{\tau}}}}
\end{mathpar}
\caption{Typing rules for values in Core \LangName{}{}.} \label{fig:core-val-types-full}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[TE-Val]{\hastype{\ensuremath{\Gamma}}{\ensuremath{v}}{\ensuremath{\tau}}}{\hastype{\ensuremath{\Gamma}}{\ensuremath{v}}{\ensuremath{\tau}}}

\inferrule[TE-Proj]{\hastype{\ensuremath{\Gamma}}{x}{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}}{\hastype{\ensuremath{\Gamma}}{\eProj{i}{x}}{\ensuremath{\tau}_i}}

\inferrule[TE-Not]{\hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\texttt{bool}}}}{\hastype{\ensuremath{\Gamma}}{\eUnop{\ensuremath{\texttt{not}}}{x}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Test]{\hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\tau}} \\ \ensuremath{\tau} \in \{\ensuremath{\texttt{uint}}, \tPtr{\ensuremath{\tau}'}\}}{\hastype{\ensuremath{\Gamma}}{\eUnop{\ensuremath{\texttt{test}}}{x}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Lop]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\texttt{bool}}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\texttt{bool}}} \\ bop \in \{\ensuremath{\texttt{\&\&}}, \ensuremath{\texttt{||}}\}}{\hastype{\ensuremath{\Gamma}}{\eBinop{x_1}{bop}{x_2}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Aop]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\texttt{uint}}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\texttt{uint}}} \\ bop \in \{\ensuremath{\texttt{+}}, \ensuremath{\texttt{-}}, \ensuremath{\texttt{*}}\}}{\hastype{\ensuremath{\Gamma}}{\eBinop{x_1}{bop}{x_2}}{\ensuremath{\texttt{uint}}}}
\end{mathpar}
\caption{Typing rules for expressions in Core \LangName{}{}.} \label{fig:core-exp-types-full}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[SE-Var]{\get{\ensuremath{R}}{x'} = \ensuremath{v} \\ \hastype{\cdot}{\ensuremath{v}}{\ensuremath{\tau}}}{\estep{x'}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}

\inferrule[SE-Pair]{\get{\ensuremath{R}}{x_1} = \ensuremath{v}_1 \\ \get{\ensuremath{R}}{x_2} = \ensuremath{v}_2 \\ \hastype{\cdot}{\ensuremath{v}_1}{\ensuremath{\tau}_1} \\ \hastype{\cdot}{\ensuremath{v}_2}{\ensuremath{\tau}_2}}{\estep{\ePair{x_1}{x_2}}{\ensuremath{R}}{x}{\ePair{\default{\ensuremath{\tau}_1}}{\default{\ensuremath{\tau}_2}}}{\ePair{\ensuremath{v}_1}{\ensuremath{v}_2}}}

\inferrule[SE-Val]{v \text{ is not a variable or pair} \\ \hastype{\cdot}{\ensuremath{v}}{\ensuremath{\tau}}}{\estep{\ensuremath{v}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}

\inferrule[SE-Proj]{\get{\ensuremath{R}}{x'} = \ePair{\ensuremath{v}_1}{\ensuremath{v}_2} \\ \hastype{\cdot}{\ensuremath{v}_i}{\ensuremath{\tau}}}{\estep{\eProj{i}{x'}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}_i}}

\inferrule[SE-Not]{\get{\ensuremath{R}}{x'} = b \\ b \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\estep{\eUnop{\ensuremath{\texttt{not}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{\neg b}}

\inferrule[SE-TestNum]{\get{\ensuremath{R}}{x'} = \vNum{n}}{\estep{\eUnop{\ensuremath{\texttt{test}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{n = 0}}

\inferrule[SE-TestPtr]{\get{\ensuremath{R}}{x'} = \vPtr{\ensuremath{\tau}}{p}}{\estep{\eUnop{\ensuremath{\texttt{test}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{\ensuremath{\texttt{false}}}}

\inferrule[SE-TestNull]{\get{\ensuremath{R}}{x'} = \vNull{\ensuremath{\tau}}}{\estep{\eUnop{\ensuremath{\texttt{test}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{\ensuremath{\texttt{true}}}}

\inferrule[SE-Lop]{\get{\ensuremath{R}}{x_1} = b_1 \\ \get{\ensuremath{R}}{x_2} = b_2 \\ bop \in \{\ensuremath{\texttt{\&\&}}, \ensuremath{\texttt{||}}\} \\ b_1, b_2 \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\estep{\eBinop{x_1}{bop}{x_2}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{b_1\ bop\ b_2}}

\inferrule[SE-Aop]{\get{\ensuremath{R}}{x_1} = \vNum{n_1} \\ \get{\ensuremath{R}}{x_2} = \vNum{n_2} \\ bop \in \{\ensuremath{\texttt{+}}, \ensuremath{\texttt{-}}, \ensuremath{\texttt{*}}\}}{\estep{\eBinop{x_1}{bop}{x_2}}{\ensuremath{R}}{x}{\vNum{0}}{\vNum{n_1\ bop\ n_2}}}
\end{mathpar}
\caption{Forward step rules of expressions in Core \LangName{}{}.} \label{fig:core-exp-eval-full}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[RE-Var]{\get{\ensuremath{R}}{x'} = \ensuremath{v} \\ \hastype{\cdot}{\ensuremath{v}}{\ensuremath{\tau}}}{\restep{x'}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}

\inferrule[RE-Pair]{\get{\ensuremath{R}}{x_1} = \ensuremath{v}_1 \\ \get{\ensuremath{R}}{x_2} = \ensuremath{v}_2 \\ \hastype{\cdot}{\ensuremath{v}_1}{\ensuremath{\tau}_1} \\ \hastype{\cdot}{\ensuremath{v}_2}{\ensuremath{\tau}_2}}{\restep{\ePair{x_1}{x_2}}{\ensuremath{R}}{x}{\ePair{\default{\ensuremath{\tau}_1}}{\default{\ensuremath{\tau}_2}}}{\ePair{\ensuremath{v}_1}{\ensuremath{v}_2}}}

\inferrule[RE-Val]{v \text{ is not a variable or pair} \\ \hastype{\cdot}{\ensuremath{v}}{\ensuremath{\tau}}}{\restep{\ensuremath{v}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}

\inferrule[RE-Proj]{\get{\ensuremath{R}}{x'} = \ePair{\ensuremath{v}_1}{\ensuremath{v}_2} \\ \hastype{\cdot}{\ensuremath{v}_i}{\ensuremath{\tau}}}{\restep{\eProj{i}{x'}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}_i}}

\inferrule[RE-Not]{\get{\ensuremath{R}}{x'} = b \\ b \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\restep{\eUnop{\ensuremath{\texttt{not}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{\neg b}}

\inferrule[RE-TestNum]{\get{\ensuremath{R}}{x'} = \vNum{n}}{\restep{\eUnop{\ensuremath{\texttt{test}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{n = 0}}

\inferrule[RE-TestPtr]{\get{\ensuremath{R}}{x'} = \vPtr{\ensuremath{\tau}}{p}}{\restep{\eUnop{\ensuremath{\texttt{test}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{\ensuremath{\texttt{false}}}}

\inferrule[RE-TestNull]{\get{\ensuremath{R}}{x'} = \vNull{\ensuremath{\tau}}}{\restep{\eUnop{\ensuremath{\texttt{test}}}{x'}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{\ensuremath{\texttt{true}}}}

\inferrule[RE-Lop]{\get{\ensuremath{R}}{x_1} = b_1 \\ \get{\ensuremath{R}}{x_2} = b_2 \\ bop \in \{\ensuremath{\texttt{\&\&}}, \ensuremath{\texttt{||}}\} \\ b_1, b_2 \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\restep{\eBinop{x_1}{bop}{x_2}}{\ensuremath{R}}{x}{\ensuremath{\texttt{false}}}{b_1\ bop\ b_2}}

\inferrule[RE-Aop]{\get{\ensuremath{R}}{x_1} = \vNum{n_1} \\ \get{\ensuremath{R}}{x_2} = \vNum{n_2} \\ bop \in \{\ensuremath{\texttt{+}}, \ensuremath{\texttt{-}}, \ensuremath{\texttt{*}}\}}{\restep{\eBinop{x_1}{bop}{x_2}}{\ensuremath{R}}{x}{\vNum{0}}{\vNum{n_1\ bop\ n_2}}}
\end{mathpar}
\caption{Reverse step rules of expressions in Core \LangName{}{}.} \label{fig:core-exp-reverse}
\end{figure}
\begin{figure}[!htb]
\begin{mathpar}
\inferrule[SS-SeqSkip]{\vphantom{\ensuremath{\Gamma}}}{\sstep{\sSeq{\ensuremath{\texttt{skip}}}{\ensuremath{s}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[SS-SeqStep]{\sstep{\ensuremath{s}_1}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'_1}{\ensuremath{R}'}{\ensuremath{M}'}}{\sstep{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\ensuremath{R}}{\ensuremath{M}}{\sSeq{\ensuremath{s}'_1}{\ensuremath{s}_2}}{\ensuremath{R}'}{\ensuremath{M}'}}

\inferrule[SS-Assign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \estep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\sstep{\sBind{x}{\ensuremath{e}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}}

\inferrule[SS-UnAssign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \restep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\sstep{\sUnbind{x}{\ensuremath{e}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[SS-Swap]{\vphantom{\ensuremath{\Gamma}}}{\sstep{\sSwap{x_1}{x_2}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_1, \ensuremath{v}_2}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_2, \ensuremath{v}_1}}{\ensuremath{M}}}

\inferrule[SS-MemSwapNull]{\get{\ensuremath{R}}{x_1} = \vNull{\ensuremath{\tau}}}{\sstep{\sMemSwap{x_1}{x_2}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[SS-MemSwapPtr]{\get{\ensuremath{R}}{x_1} = \vPtr{\ensuremath{\tau}}{p}}{\sstep{\sMemSwap{x_1}{x_2}}{\subst{\ensuremath{R}}{x_2}{\ensuremath{v}}}{\subst{\ensuremath{M}}{p}{\ensuremath{v}'}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x_2}{\ensuremath{v}'}}{\subst{\ensuremath{M}}{p}{\ensuremath{v}}}}

\inferrule[SS-IfTrue]{\get{\ensuremath{R}}{x} = \ensuremath{\texttt{true}}}{\sstep{\sIf{x}{\ensuremath{s}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[SS-IfFalse]{\get{\ensuremath{R}}{x} = \ensuremath{\texttt{false}}}{\sstep{\sIf{x}{\ensuremath{s}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}
\end{mathpar}
\caption{Forward step rules of statements in Core \LangName{}{}.} \label{fig:core-stmt-step-full}
\end{figure}
\begin{figure}[!htb]
\begin{mathpar}
\inferrule[RS-SeqSkip]{\vphantom{\ensuremath{\Gamma}}}{\rsstep{\sSeq{\ensuremath{s}}{\ensuremath{\texttt{skip}}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[RS-SeqStep]{\rsstep{\ensuremath{s}_2}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}'_2}{\ensuremath{R}'}{\ensuremath{M}'}}{\rsstep{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\ensuremath{R}}{\ensuremath{M}}{\sSeq{\ensuremath{s}_1}{\ensuremath{s}'_2}}{\ensuremath{R}'}{\ensuremath{M}'}}

\inferrule[RS-Assign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \restep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\rsstep{\sBind{x}{\ensuremath{e}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}}

\inferrule[RS-UnAssign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \estep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\rsstep{\sUnbind{x}{\ensuremath{e}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[RS-Swap]{\vphantom{\ensuremath{\Gamma}}}{\rsstep{\sSwap{x_1}{x_2}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_1, \ensuremath{v}_2}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x_1, x_2}{\ensuremath{v}_2, \ensuremath{v}_1}}{\ensuremath{M}}}

\inferrule[RS-MemSwapNull]{\get{\ensuremath{R}}{x_1} = \vNull{\ensuremath{\tau}}}{\rsstep{\sMemSwap{x_1}{x_2}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[RS-MemSwapPtr]{\get{\ensuremath{R}}{x_1} = \vPtr{\ensuremath{\tau}}{p}}{\rsstep{\sMemSwap{x_1}{x_2}}{\subst{\ensuremath{R}}{x_2}{\ensuremath{v}}}{\subst{\ensuremath{M}}{p}{\ensuremath{v}'}}{\ensuremath{\texttt{skip}}}{\subst{\ensuremath{R}}{x_2}{\ensuremath{v}'}}{\subst{\ensuremath{M}}{p}{\ensuremath{v}}}}

\inferrule[RS-IfTrue]{\get{\ensuremath{R}}{x} = \ensuremath{\texttt{true}}}{\rsstep{\sIf{x}{\ensuremath{s}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{s}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[RS-IfFalse]{\get{\ensuremath{R}}{x} = \ensuremath{\texttt{false}}}{\rsstep{\sIf{x}{\ensuremath{s}}}{\ensuremath{R}}{\ensuremath{M}}{\ensuremath{\texttt{skip}}}{\ensuremath{R}}{\ensuremath{M}}}
\end{mathpar}
\caption{Reverse step rules of statements in Core \LangName{}{}.} \label{fig:core-stmt-reverse-full}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[Stuck-SeqStep]{\sstepstuck{\ensuremath{s}_1}{\ensuremath{R}}{\ensuremath{M}}}{\sstepstuck{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\ensuremath{R}}{\ensuremath{M}}}

\inferrule[Stuck-UnAssign]{\hastype{\regtypes{\ensuremath{R}}}{\ensuremath{e}}{\ensuremath{\tau}} \\ \lnot \restep{\ensuremath{e}}{\ensuremath{R}}{x}{\default{\ensuremath{\tau}}}{\ensuremath{v}}}{\sstepstuck{\sUnbind{x}{\ensuremath{e}}}{\subst{\ensuremath{R}}{x}{\ensuremath{v}}}{\ensuremath{M}}}
\end{mathpar}
\caption{Stuck steps in Core \LangName{}{}.}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
    \inferrule[TE-Alloc]{\vphantom{\ensuremath{\Gamma}}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eAlloc{\ensuremath{\tau}}}{\tPtr{\ensuremath{\tau}}}}
\end{mathpar}
\caption{Typing rule for allocation in Core \LangName{}{}.}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[TypOk-Var]{\vphantom{\ensuremath{\Gamma}}}{\typeok{\ensuremath{\Delta}, t}{t}}

\inferrule[TypOk-Base]{\ensuremath{\tau} \in \{\ensuremath{()}, \ensuremath{\texttt{uint}}, \ensuremath{\texttt{bool}}\}}{\typeok{\ensuremath{\Delta}}{\ensuremath{\tau}}}

\inferrule[TypOk-Pair]{\typeok{\ensuremath{\Delta}}{\ensuremath{\tau}_1} \quad \typeok{\ensuremath{\Delta}}{\ensuremath{\tau}_2}}{\typeok{\ensuremath{\Delta}}{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}}

\inferrule[TypOk-Ptr]{\typeok{\ensuremath{\Delta}}{\ensuremath{\tau}}}{\typeok{\ensuremath{\Delta}}{\tPtr{\ensuremath{\tau}}}}

\inferrule[TypOk-Ind]{\typeok{\ensuremath{\Delta}, t}{\ensuremath{\tau}} \\\\ t \notin \exposed{\ensuremath{\tau}}}{\typeok{\ensuremath{\Delta}}{\tInd{t}{\ensuremath{\tau}}}}
\end{mathpar}
\begin{align*}
& \exposed{\ensuremath{()}} = \exposed{\ensuremath{\texttt{uint}}} = \exposed{\ensuremath{\texttt{bool}}} = \exposed{\tPtr{\ensuremath{\tau}}} = \emptyset \\
& \exposed{t} = \{t\} \quad \exposed{\tInd{t}{\ensuremath{\tau}}} = \exposed{\ensuremath{\tau}} \setminus \{t\} \quad \exposed{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}} = \exposed{\ensuremath{\tau}_1} \cup \exposed{\ensuremath{\tau}_2}
\end{align*}
\caption{Well-formation rules for types in Tower{}.} \label{fig:main-type-ok}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[TypEq-Refl]{\ensuremath{\tau} \in \{t, \ensuremath{()}, \ensuremath{\texttt{uint}}, \ensuremath{\texttt{bool}}\}}{\typeequiv{\ensuremath{\tau}}{\ensuremath{\tau}}}

\inferrule[TypEq-Pair]{\typeequiv{\ensuremath{\tau}_1}{\ensuremath{\tau}'_1} \\ \typeequiv{\ensuremath{\tau}_2}{\ensuremath{\tau}'_2}}{\typeequiv{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}{\tPair{\ensuremath{\tau}'_1}{\ensuremath{\tau}'_2}}}

\inferrule[TypEq-Ptr]{\typeequiv{\ensuremath{\tau}}{\ensuremath{\tau}'}}{\typeequiv{\tPtr{\ensuremath{\tau}}}{\tPtr{\ensuremath{\tau}'}}}

\inferrule[TypEq-Ind]{\typeequiv{\ensuremath{\tau}}{\ensuremath{\tau}'}}{\typeequiv{\tInd{t}{\ensuremath{\tau}}}{\tInd{t}{\ensuremath{\tau}'}}}

\inferrule[TypEq-Unfold]{\vphantom{\ensuremath{\Gamma}}}{\typeequiv{\tInd{t}{\ensuremath{\tau}}}{\subst{\ensuremath{\tau}}{t}{\tInd{t}{\ensuremath{\tau}}}}}

\inferrule[TypEq-Sym]{\typeequiv{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}{\typeequiv{\ensuremath{\tau}_2}{\ensuremath{\tau}_1}}

\inferrule[TypEq-Trans]{\typeequiv{\ensuremath{\tau}_1}{\ensuremath{\tau}_2} \\ \typeequiv{\ensuremath{\tau}_2}{\ensuremath{\tau}_3}}{\typeequiv{\ensuremath{\tau}_1}{\ensuremath{\tau}_3}}
\end{mathpar}
\caption{Type equivalence rules in Tower{}.} \label{fig:main-type-equiv}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[TV-Eq]{\typeequiv{\ensuremath{\tau}_1}{\ensuremath{\tau}_2} \\ \hastype{\ensuremath{\Gamma}}{\ensuremath{v}}{\ensuremath{\tau}_1}}{\hastype{\ensuremath{\Gamma}}{\ensuremath{v}}{\ensuremath{\tau}_2}}

\inferrule[TV-Var]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}, x : \ensuremath{\tau}}{x}{\ensuremath{\tau}}}

\inferrule[TV-Unit]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\ensuremath{()}}{\ensuremath{()}}}

\inferrule[TV-Pair]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\tau}_2}}{\hastype{\ensuremath{\Gamma}}{\ePair{x_1}{x_2}}{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}}

\inferrule[TV-Num]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vNum{n}}{\ensuremath{\texttt{uint}}}}

\inferrule[TV-Bool]{b \in \{\ensuremath{\texttt{true}}, \ensuremath{\texttt{false}}\}}{\hastype{\ensuremath{\Gamma}}{b}{\ensuremath{\texttt{bool}}}}

\inferrule[TV-Null]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vNull{\ensuremath{\tau}}}{\tPtr{\ensuremath{\tau}}}}

\inferrule[TV-Ptr]{\vphantom{\ensuremath{\Gamma}}}{\hastype{\ensuremath{\Gamma}}{\vPtr{\ensuremath{\tau}}{p}}{\tPtr{\ensuremath{\tau}}}}
\end{mathpar}
\caption{Typing rules for values in Tower{}.} \label{fig:main-val-types-full}
\end{figure}

\begin{figure}
\begin{mathpar}
\inferrule[TE-Val]{\hastype{\ensuremath{\Gamma}}{\ensuremath{v}}{\ensuremath{\tau}}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{v}}{\ensuremath{\tau}}}

\inferrule[TE-Proj]{\hastype{\ensuremath{\Gamma}}{x}{\tPair{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eProj{i}{x}}{\ensuremath{\tau}_i}}

\inferrule[TE-Not]{\hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\texttt{bool}}}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eUnop{\ensuremath{\texttt{not}}}{x}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Test]{\hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\tau}} \\ \ensuremath{\tau} \in \{\ensuremath{\texttt{uint}}, \tPtr{\ensuremath{\tau}'}\}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eUnop{\ensuremath{\texttt{test}}}{x}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Lop]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\texttt{bool}}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\texttt{bool}}} \\ bop \in \{\ensuremath{\texttt{\&\&}}, \ensuremath{\texttt{||}}\}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eBinop{x_1}{bop}{x_2}}{\ensuremath{\texttt{bool}}}}

\inferrule[TE-Aop]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\texttt{uint}}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\texttt{uint}}} \\ bop \in \{\ensuremath{\texttt{+}}, \ensuremath{\texttt{-}}, \ensuremath{\texttt{*}}\}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eBinop{x_1}{bop}{x_2}}{\ensuremath{\texttt{uint}}}}

\inferrule[TE-Alloc]{\vphantom{\ensuremath{\Gamma}}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eAlloc{\ensuremath{\tau}}}{\tPtr{\ensuremath{\tau}}}}

\inferrule[TE-CallUnbounded]{f_1 \neq f_2 \\ \get{\ensuremath{\Phi}}{f_2} = (\textsf{None}, ((\ensuremath{\tau}_1, \ldots, \ensuremath{\tau}_k), \ensuremath{\tau})) \\\\ \hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \quad \cdots \quad \hastype{\ensuremath{\Gamma}}{x_k}{\ensuremath{\tau}_k}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f_1}{\eCall{f_2}{}{x_1, \ldots, x_k}}{\ensuremath{\tau}}}

\inferrule[TE-CallBounded]{\ensuremath{\beta} = n \text{ or } \ensuremath{\beta} = \ensuremath{b} \text{ or } \ensuremath{b} - n \text{ where } \textsf{fst}(\get{\ensuremath{\Phi}}{f_1}) = \ensuremath{b} \\\\ f_1 \neq f_2 \\ \get{\ensuremath{\Phi}}{f_2} = (\textsf{Some}\ b_2, ((\ensuremath{\tau}_1, \ldots, \ensuremath{\tau}_k), \ensuremath{\tau})) \\\\ \hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \quad \cdots \quad \hastype{\ensuremath{\Gamma}}{x_k}{\ensuremath{\tau}_k}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f_1}{\eCall{f_2}{\ensuremath{\beta}}{x_1, \ldots, x_k}}{\ensuremath{\tau}}}

\inferrule[TE-CallSelf]{\get{\ensuremath{\Phi}}{f} = (\textsf{Some}\ b, ((\ensuremath{\tau}_1, \ldots, \ensuremath{\tau}_k), \ensuremath{\tau})) \\\\ \hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \quad \cdots \quad \hastype{\ensuremath{\Gamma}}{x_k}{\ensuremath{\tau}_k}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eCall{f}{\ensuremath{b} - n}{x_1, \ldots, x_k}}{\ensuremath{\tau}}}
\end{mathpar}
\caption{Typing rules for expressions in Tower{}.} \label{fig:main-exp-types-full}
\end{figure}

\begin{figure}[!htb]
\begin{mathpar}
\inferrule[S-Skip]{\vphantom{\ensuremath{\Gamma}}}{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{\texttt{skip}}}{\ensuremath{\Gamma}}}

\inferrule[S-Seq]{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{s}_1}{\ensuremath{\Gamma}'} \\ \stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}'}{f}{\ensuremath{s}_2}{\ensuremath{\Gamma}''}}{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\sSeq{\ensuremath{s}_1}{\ensuremath{s}_2}}{\ensuremath{\Gamma}''}}

\inferrule[S-Assign]{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{e}}{\ensuremath{\tau}} \\ x \notin \ensuremath{\Gamma}}{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\sBind{x}{e}}{\ensuremath{\Gamma}, x : \ensuremath{\tau}}}

\inferrule[S-UnAssign]{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{e}}{\ensuremath{\tau}} \\ x \notin \ensuremath{\Gamma}}{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}, x : \ensuremath{\tau}}{f}{\sUnbind{x}{e}}{\ensuremath{\Gamma}}}

\inferrule[S-Swap]{\hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\tau}}}{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\sSwap{x_1}{x_2}}{\ensuremath{\Gamma}}}

\inferrule[S-MemSwap]{\hastype{\ensuremath{\Gamma}}{x_1}{\tPtr{\ensuremath{\tau}}} \\ \hastype{\ensuremath{\Gamma}}{x_2}{\ensuremath{\tau}}}{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\sMemSwap{x_1}{x_2}}{\ensuremath{\Gamma}}}

\inferrule[S-If]{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{s}}{\ensuremath{\Gamma}} \\ \hastype{\ensuremath{\Gamma}}{x}{\ensuremath{\texttt{bool}}} \\ x \notin \modified{\ensuremath{s}}}{\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\sIf{x}{s}}{\ensuremath{\Gamma}}}

\inferrule[S-Return]{\vphantom{\ensuremath{\Gamma}}}{\stmtokf{\ensuremath{\Phi}}{x : \ensuremath{\tau}}{f}{\sReturn{x}}{\cdot}}
\end{mathpar}
\caption{Well-formation rules for statements in Tower{}.} \label{fig:main-stmt-ok}
\end{figure}

\FloatBarrier

\section{Limitations} \label{sec:future-work}

\paragraph{Error Checking}
Programming with memory causes numerous errors such as null pointer dereference, use after free, and out of memory. Detecting such errors is difficult in quantum programs, which cannot use exceptional control flow. Consequently, Tower{} defines a dereference of a null pointer to be a no-op and does not dynamically enforce memory safety. Developments in quantum runtime error checking such as~\citet{assertions} may enable detection of memory errors.

\paragraph{Memory Management}
In Tower{}, the developer must manually reset and deallocate memory, which raises the possibility of automatic memory reclamation. Unfortunately, classical garbage collection traverses the heap, which has a high time cost. Also, erasing information cannot be performed reversibly without uncomputation, which is difficult after memory has become garbage.

Boson{} incurs internal and external heap fragmentation when allocating variable-sized blocks of memory. Practical dynamic memory management in quantum programs must reconcile space inefficiency of simple allocation schemes with the expense of traversing the heap.

\section{Introduction} \label{sec:intro}

Algorithms for quantum computers promise computational advantages in areas ranging from integer factorization~\citep{shor1997} and search~\citep{grover} to cryptography~\citep{bennett}, linear algebra~\citep{Harrow_2009}, physical simulation~\citep{simulation-physics,simulation-chem}, and combinatorial optimization~\citep{farhi2014}. Enabling practical realization of these algorithms on quantum hardware is a major aim of \emph{quantum programming languages}, in which a developer may write programs that execute on a quantum computer.

The principles of quantum mechanics specify how a quantum computer manipulates \emph{quantum states} consisting of \emph{qubits}, the quantum analogs of classical bits. A quantum state exists in a \emph{superposition}, a weighted sum over classical states. The computer may evolve the state using \emph{unitary operators}, or it may \emph{measure} the state, which causes a superposition to assume a classical state with probability derived mathematically from the weight ascribed to that state in the sum.

\subsection{Data Structures and Quantum Algorithms}

Existing quantum programming languages~\citep{qsharp, quipper, qwire, liquid, qml, quantum-lambda-calc, silq} build abstractions for individual qubits and primitive data types such as integers.
However, emerging quantum algorithms incorporate abstract data structures for sake of implementation and efficiency. The concrete representation of such a data structure is a classically linked structure in random-access memory, defined inductively and constructed by dynamic allocation.

For example, the set data structure can maintain a duplicate-free collection of items, check an element for membership in the collection, and add and remove elements from the collection.
Examples of quantum algorithms that depend critically on sets include \citet{ambainis2003}, who presents an $O(n^{2/3})$ quantum algorithm for element distinctness that improves over the $\Omega(n)$ classical bound; \citet{bernstein2013}, who present a quantum algorithm for subset sum that beats the classical complexity of $O(2^{n/4})$; and \citet{aaronson2019}, who present an $\tilde{O}(n^{2/3})$ quantum algorithm for closest pair, improving over $O(n\log n)$ classically. Each of these algorithms relies on an implementation of sets whose operations execute in $O(\log n)$ time.

To date, no quantum programming language provides abstractions for constructing and manipulating sets and other abstract data types, a hurdle to the realization of these algorithms.

\subsection{Three Requirements for Data Structures}

Importantly, not all classical data structure implementations are compatible with quantum programming. \citet{ambainis2003} identifies a data structure appropriate for use in a quantum algorithm as one that satisfies three properties: \emph{reversibility}, \emph{history independence} and \emph{bounded-time execution}.

\paragraph{Reversible Operation}

The operations of the data structure must each be \emph{reversible}, meaning it can be executed forwards or backwards to produce or undo its effect on the program state.

For a program to execute on a quantum computer, the program must first be compiled into a sequence of primitive \emph{quantum gates}. Each gate corresponds to either a measurement or a unitary operator over the program state. According to quantum mechanics, measurement does not preserve the superposition of program data, and instead collapses the data into a classical state, which causes algorithms such as~\citet{ambainis2003} to return incorrect results.

Thus, when a program executes an operation on data in superposition, the operation must correspond to a unitary operator, which has an inverse by definition. As a consequence, the operations of a data structure in superposition must be reversible.

\paragraph{History-Independent Representation}

The representation of the data structure must be \emph{history-independent}, meaning it assigns each instance of the data structure a single unique physical representation in memory that is insensitive to the history of operations performed on it.

History independence is necessary to the correctness or performance of certain algorithms. For example, \citet{ambainis2003} relies on quantum \emph{interference}, the phenomenon in which weights of identical classical states in a superposition combine or cancel. The algorithm requires interference to occur between sets containing the same elements. However, if semantically equivalent sets have distinct physical representations, interference does not occur, resulting in incorrect outputs.

\paragraph{Bounded-Time Execution}

A data structure operation must execute in \emph{bounded time}, meaning its execution time is bounded by classical parameters not dependent on quantum data.

An inductive definition of a data structure typically corresponds to recursive implementations of its operations. Recursion enables an operation to use variable time complexity to traverse and manipulate a variable-sized data structure.
However, a quantum computer does not natively support recursion and must first classically convert the program to a loop-free form. Hence, all recursion in the program must be bounded by classically determined parameters.

\subsection{Tower{}: Data Structures in Quantum Superposition}

\paragraph{Core \LangName{}}

We present Core \LangName{}{}, the first language that enables quantum programming with data in random-access memory. It enables the construction and manipulation of pointer-based, linked data, by means of operations for integers, pointers, and control flow.

\paragraph{Reversibility}

In Core \LangName{}{}, every program that can execute forwards can also execute backwards.
A developer may compute an expression by assigning it to a variable, or \emph{uncompute} an expression, which reverses the computation, by \emph{un-assigning} it from a variable. Other features enable the developer to swap two variables, or to swap a variable with the content of memory at an address.

We present a fully reversible operational semantics of Core \LangName{}{}. Each operator has a reverse within the syntax, meaning a developer may write a program and derive another program with reversed semantics using the syntactic transformation of \emph{program inversion}.

We provide a translation from a valid Core \LangName{}{} program to a unitary operator that can execute on a quantum computer. Specifically, the resulting operator acts uniformly across each classical program state in a superposition, and may then be embedded within a larger quantum algorithm that creates and manipulates weights of superpositions.

\paragraph{Boson}

We present Boson{}, the first memory allocator that enables reversible, history-independent, and constant-time dynamic memory allocation in superposition.
A developer may invoke Boson{} to write a history-independent implementation of a data structure.

\paragraph{History Independence}

To leverage Boson{}, the developer constructs dynamically allocated, linked data whose linking structure is in one-to-one correspondence with semantic data structure instances. At runtime, Boson{} stores data into superpositions of allocation sites that are chosen to guarantee that the instance's physical memory representation, including the values of pointers, is unique.

Classically, a memory allocator may establish history independence by randomizing allocation addresses. The implementation of Boson{} lifts randomization to quantum superposition via \emph{symmetrization}, an approach from quantum simulation~\citep{abrams1997,Berry2017ImprovedTF}.

\paragraph{Tower}

We combine Core \LangName{}{} and Boson{} to build Tower{}, a programming language for quantum programming with data structures. Tower{} features inductive types and recursive functions that enable the developer to recursively define data structures and operations.

\paragraph{Bounded-Time Execution}
The type system of Tower{} ensures that all recursive functions are bounded in size by classical parameters. A Tower{} program lowers to Core \LangName{}{} by unrolling recursive calls, meaning it corresponds to a bounded-size quantum circuit.

\subsection{Ground{}: Data Structure Library}

We use Tower{} to implement Ground{}, the first quantum library of data structures, consisting of lists, stacks, queues, strings, and sets.
Of note, we demonstrate the first executable implementation of sets that is reversible, history-independent, and bounded-time, using radix trees~\citep{morrison} as proposed by~\citet{bernstein2013}.
Prior to this work, we are not aware of any existing quantum implementation of the set data structure that satisfies all three properties.

As a case study, we describe three challenges we encountered during the development process that do not arise in classical programming, as well as techniques to overcome them:

\begin{itemize}
    \item \emph{Recursive uncomputation} means that functions that uncompute the results of recursive calls may incur exponential slowdown in time complexity. We instead structure a program to avoid having recursive calls be temporary values.
    \item \emph{Mutated uncomputation} means that directly uncomputing temporary variables after the program state has been mutated may result in incorrect outcomes. We instead correctly uncompute values using context from the updated program state.
    \item \emph{Branch sequentialization} means that the time complexity of a conditionally branching quantum program is equal to the sum and not the maximum of its branches. To prevent inefficiency, we structure a program to avoid recursion under branches.
\end{itemize}

\pagebreak

\subsection{Contributions}

In this work we present the following contributions:
\begin{itemize}
    \item \emph{Core \LangName{}{}}. We present Core \LangName{}{}, the first language for quantum programming with random-access memory. We formalize its type system, reversible operational semantics, program inversion transformation, and translation into a unitary quantum circuit.
    \item \emph{Boson{}}. We present Boson{}, the first memory allocator that enables reversible, history-independent, and constant-time dynamic memory allocation in superposition. We present the implementation of Boson{} using techniques from quantum simulation.
    \item \emph{Tower{}}. We present Tower{}, a language that enables bounded-time quantum programming with inductive data structures. We formalize its type system, which verifies that recursion is classically bounded, and its lowering into Core \LangName{}{}.
    \item \emph{Ground{}}. We present Ground{}, the first quantum library of abstract data structures, including lists, stacks, queues, strings, and sets. We present the first executable set implementation satisfying reversibility, history independence, and bounded-time execution.
    \item \emph{Case Study}. We characterize three challenges we faced in the library implementation that do not arise in classical programming -- recursive uncomputation, mutated uncomputation, and branch sequentialization -- and techniques to overcome them.
\end{itemize}

\paragraph{Summary}

Our work establishes programming abstractions for data structures in quantum superposition in the form of language design, and provides the first quantum library of fundamental data structures. Together, Tower{}, Boson{}, and Ground{} enable developers to implement algorithms and construct quantum software utilizing familiar and useful data structures.

\section{Tower{}: Inductive Data Types} \label{sec:main-semantics}

In this section, we present Tower{}, which features inductive types and bounded recursive functions.

\subsection{Syntax}

The syntax of Tower{} adds new types, expressions and statements, as well as function declarations $\ensuremath{d}$, \emph{recursion bounds} $\ensuremath{\beta}$, and programs $\ensuremath{p}$. Recursion bounds enable Tower{} to guarantee that all programs are bounded by classically known parameters.
\begin{alignat*}{3}
    \textsf{Type}\ \ensuremath{\tau} \Coloneqq{} & \cdots  \mid \tInd{t}{\ensuremath{\tau}} \quad & \textsf{Declaration}\ \ensuremath{d} \Coloneqq{} & \dFun{f}{\ensuremath{b}?}{x_1 : \ensuremath{\tau}_1, \ldots, x_k : \ensuremath{\tau}_k}{\ensuremath{\tau}}{\ensuremath{s}} \\
    \textsf{Expression}\ \ensuremath{e} \Coloneqq{} & \cdots \mid \eCall{f}{\ensuremath{\beta}?}{x_1, \ldots, x_k} \quad & \textsf{Bound}\ \ensuremath{\beta} \Coloneqq{} & \ensuremath{b} \mid n \mid \ensuremath{b} - n' \hspace{1em} (n \in \mathbb{N}, n' \in \mathbb{N}^+) \\
    \textsf{Statement}\ \ensuremath{s} \Coloneqq{} & \cdots \mid \sReturn{x} \quad & \textsf{Program}\ \ensuremath{p} \Coloneqq{} & \ensuremath{d} \text{  } \ensuremath{p} \mid \dFun{\texttt{main}}{}{x : \ensuremath{\tau}}{\ensuremath{\tau}'}{\ensuremath{s}}
\end{alignat*}
\paragraph{Types}
The type $\tInd{t}{\ensuremath{\tau}}$ is an inductive type in which $t$ may appear in $\ensuremath{\tau}$.

\paragraph{Expressions}
The expression $\eCall{f}{\ensuremath{\beta}?}{x_1, \ldots, x_k}$ invokes function $f$ on arguments $x_1, \ldots x_k$ with recursion bound $\ensuremath{\beta}$, or no bound if $\ensuremath{\beta}$ is absent.

\paragraph{Statements}
The statement $\sReturn{x}$ returns the value of $x$ to the caller.

\paragraph{Declarations}
The declaration $\dFun{f}{\ensuremath{b}?}{x_1 : \ensuremath{\tau}_1, \ldots, x_k : \ensuremath{\tau}_k}{\ensuremath{\tau}}{\ensuremath{s}}$ declares a function named $f$ with recursion bound $\ensuremath{b}$ (or no bound if absent), arguments $x_1, \ldots, x_k$ with types $\ensuremath{\tau}_1, \ldots, \ensuremath{\tau}_k$ respectively, return type $\ensuremath{\tau}$, and body $\ensuremath{s}$. A function body must contain exactly one return statement, as the final statement. Tower{} permits recursive, but not mutually recursive, functions.\footnote{The presented type system of Tower{} could be modified straightforwardly to support mutual recursion.}

\paragraph{Bounds}
A recursion bound may be a variable $\ensuremath{b}$, a classical integer $n$, or their difference.

\paragraph{Programs}
A program is a series of function declarations followed by the entry point \texttt{main}.

\pagebreak

\subsection{Type System}

The type system defines valid inductive types and enforces that all recursion is classically bounded.

\paragraph{Type Formation}
In~\Cref{sec:full-semantics}, we define the well-formation of types. A context $\ensuremath{\Delta}$ is a set of type variables currently in scope. The judgment $\typeok{\ensuremath{\Delta}}{\ensuremath{\tau}}$ states that under context $\ensuremath{\Delta}$, the type $\ensuremath{\tau}$ is well-formed. All rules are standard except the case for inductive types, which additionally requires that $t$ may only appear under a pointer indirection.

For example, the type of lists of integers is $\texttt{list} \triangleq \tInd{t}{\tPair{\ensuremath{\texttt{uint}}}{\tPtr{t}}}$, in which we require that the self-reference $t$ must occur under a pointer, similarly to structure definitions in C.
We interpret inductive types equi-recursively. For example, we equate the list type $\texttt{list} \triangleq \tInd{t}{\tPair{\ensuremath{\texttt{uint}}}{\tPtr{t}}}$ with its unfolding $\tPair{\ensuremath{\texttt{uint}}}{\tPtr{\texttt{list}}}$. In~\Cref{sec:full-semantics}, we define the judgment $\typeequiv{\ensuremath{\tau}_1}{\ensuremath{\tau}_2}$, an equivalence relation that is compatible with unfolding inductive types. The default value of an inductive type, $\default{\tInd{t}{\ensuremath{\tau}}}$, is defined to be the default value of its unfolding, $\default{\subst{\ensuremath{\tau}}{t}{\tInd{t}{\ensuremath{\tau}}}}$.

\paragraph{Recursive Functions}

The type system of Tower{} introduces a function context $\ensuremath{\Phi}$ that maps functions to their recursion bound variable (if present), argument list, and return type, and augments the typing judgments with the function context $\ensuremath{\Phi}$ and the function $f$ being type-checked.

\begin{figure}
\begin{mathpar}
\inferrule[TE-CallUnbounded]{f_1 \neq f_2 \\ \get{\ensuremath{\Phi}}{f_2} = (\textsf{None}, ((\ensuremath{\tau}_1, \ldots, \ensuremath{\tau}_k), \ensuremath{\tau})) \\\\ \hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \quad \cdots \quad \hastype{\ensuremath{\Gamma}}{x_k}{\ensuremath{\tau}_k}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f_1}{\eCall{f_2}{}{x_1, \ldots, x_k}}{\ensuremath{\tau}}}

\inferrule[TE-CallBounded]{\ensuremath{\beta} = n \text{ or } \ensuremath{\beta} = \ensuremath{b} \text{ or } \ensuremath{b} - n \text{ where } \textsf{fst}(\get{\ensuremath{\Phi}}{f_1}) = \ensuremath{b} \\\\ f_1 \neq f_2 \\ \get{\ensuremath{\Phi}}{f_2} = (\textsf{Some}\ b_2, ((\ensuremath{\tau}_1, \ldots, \ensuremath{\tau}_k), \ensuremath{\tau})) \\\\ \hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \quad \cdots \quad \hastype{\ensuremath{\Gamma}}{x_k}{\ensuremath{\tau}_k}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f_1}{\eCall{f_2}{\ensuremath{\beta}}{x_1, \ldots, x_k}}{\ensuremath{\tau}}}

\inferrule[TE-CallSelf]{\get{\ensuremath{\Phi}}{f} = (\textsf{Some}\ b, ((\ensuremath{\tau}_1, \ldots, \ensuremath{\tau}_k), \ensuremath{\tau})) \\ \hastype{\ensuremath{\Gamma}}{x_1}{\ensuremath{\tau}_1} \quad \cdots \quad \hastype{\ensuremath{\Gamma}}{x_k}{\ensuremath{\tau}_k}}{\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\eCall{f}{\ensuremath{b} - n}{x_1, \ldots, x_k}}{\ensuremath{\tau}}}
\end{mathpar}
\caption{Selected typing rules for expressions in Tower{}. The full definition is presented in~\Cref{sec:full-semantics}.} \label{fig:main-exp-types}
\end{figure}

In~\Cref{fig:main-exp-types}, we define the new typing judgment for expressions. The judgment $\hastypef{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{e}}{\ensuremath{\tau}}$ states that under function context $\ensuremath{\Phi}$ and context $\ensuremath{\Gamma}$, inside function $f$, expression $\ensuremath{e}$ has type $\ensuremath{\tau}$. Most of the rules simply add $\ensuremath{\Phi}$ and $f$, and we show only the new rules for function calls.

If the function being called, $f_2$, has no bound, it must be called with no bound and the correct arguments. If it has a bound, it must be called with a bound, which in turn may refer only to the bound variable of the caller function $f_1$. In the last rule, the function $f$ is making a recursive call, which requires the bound to be smaller than the bound variable $\ensuremath{b}$.\footnotemark
\footnotetext{A recursive call typically provides the bound $\ensuremath{b} - 1$.}

In~\Cref{sec:full-semantics}, we define the new judgment for well-formation of statements. The judgment $\stmtokf{\ensuremath{\Phi}}{\ensuremath{\Gamma}}{f}{\ensuremath{s}}{\ensuremath{\Gamma}'}$ states that under $\ensuremath{\Phi}$ and $\ensuremath{\Gamma}$, inside function $f$, statement $\ensuremath{s}$ is well-formed and yields new context $\ensuremath{\Gamma}'$. Most of the rules simply add $\ensuremath{\Phi}$ and $f$. The new rule for \texttt{return} requires that the context contains only the returned variable, and yields an empty context.

\subsection{Translation into Core \LangName{}{}}

Tower{}'s dynamic semantics is defined by translation into Core \LangName{}{}. We translate recursive functions, starting from \texttt{main}, by inlining.

In the general case, a function call has a specified recursion bound.
Given a function call $\sBind{x}{\eCall{f}{n}{x_1, \ldots, x_k}}$, the translator looks up the definition of $f$ and renames its arguments and return value to be $\dFun{f}{\ensuremath{b}}{x_1 : \ensuremath{\tau}_1, \ldots, x_k : \ensuremath{\tau}_k}{\ensuremath{\tau}}{\sSeq{\ensuremath{s}}{\sReturn{x}}}$. It also renames the local variables of $f$ to avoid conflicts with the caller. It then inlines $\ensuremath{s}$ into the caller, replacing instances of $\ensuremath{b}$ with $n$. It recursively expands introduced function calls until the recursion bound reaches zero, and it replaces expressions $\eCall{f}{0}{x_1, \ldots, x_k}$ with $\default{\ensuremath{\tau}}$.
A reverse function call $\sUnbind{x}{\eCall{f}{n}{x_1, \ldots, x_k}}$ is similar, except that the body of $f$ is inverted (\Cref{sec:program-inversion}) before it is inlined.
\begin{theorem}
    In a well-typed program, the process of inlining recursive calls always terminates.
\end{theorem}
\begin{proof}
    Every recursive call has a bound strictly smaller than the bound of the function definition. A call with bound zero terminates immediately. By induction, all other recursive calls terminate.
\end{proof}
As a result, a well-typed Tower{} program executes in time bounded by classical parameters and can be converted into a quantum circuit.
Additional features of Tower{}, such as \lstinline{with}-\lstinline{do} blocks, nested expressions, and patterns, also lower into Core \LangName{}{} and are described in~\Cref{sec:additional-features}.

\section{Boson{}: History-Independent Quantum Memory Allocation} \label{sec:memory-allocation}

In this section, we present Boson{}, a reversible, history-independent, and constant-time memory allocator for quantum programs. Boson{} guarantees that a data structure with a unique logical linking structure also has a unique physical memory representation and is history-independent.

\subsection{Syntax and Types}

We augment Core \LangName{}{} syntax with dynamic memory allocation:
\begin{align*}
    \textsf{Expression}\ \ensuremath{e} \Coloneqq{} & \cdots \mid \eAlloc{\ensuremath{\tau}}
\end{align*}
The expression $\eAlloc{\ensuremath{\tau}}$ allocates zero-initialized space for a value of type $\ensuremath{\tau}$.
In~\Cref{sec:full-semantics}, we update the expression typing judgment to specify that $\eAlloc{\ensuremath{\tau}}$ has the type of pointer to $\ensuremath{\tau}$.

\subsection{Free List Allocator}

The following strategy implements \texttt{alloc} reversibly and in constant time, but is not yet history-independent.
Before the program executes, the qRAM is divided into a heap of $n + 1$ blocks of size $k$, the word size of the system, and the blocks are initialized to a sequence $[\vNull{}$, $\vPtr{}{2}$, $\vPtr{}{3}, \ldots,$ $\vPtr{}{n}$, $\vNull{}]$. A designated \emph{allocation register} denoted \texttt{hp} is initialized to $\vPtr{}{1}$.

\paragraph{Allocation}
The implementation of $\sBind{\texttt{x}}{\eAlloc{\ensuremath{\tau}}}$, assuming $\ensuremath{\tau}$ is word-sized, is:

\noindent\begin{minipage}{\textwidth}
\begin{lstlisting}[style=nonum]
let x <- null;
x <-> hp;  /* x <- address of first free block, hp <- null */
*x <-> hp; /* hp <- address of next free block, *x <- null */
\end{lstlisting}
\end{minipage}

\noindent
The first line stores in \texttt{x} the address of the first available free block and stores zero in \texttt{hp}. The second line stores into \texttt{hp} the value at memory address \texttt{x}, which is the address of the next available block, and stores zero into memory at address \texttt{x}. Then, \texttt{x} is returned to the program.

This allocator is reversible and performs memory allocation in constant time. The reversal of the allocator deallocates memory by putting the block at the head of the free list. To support variable-sized allocation, it partitions the heap into sections of blocks whose sizes are different powers of two, and allocates from the appropriate free list.

\subsection{History Independence}

To determine whether the just-proposed allocator enables history-independent data structures, we view the heap itself as an abstract data structure, whose operations are allocation and deallocation, and the allocator as its implementation. In fact, the free list allocator is not history-independent, as the empty heap has multiple distinct memory representations:

\noindent\begin{minipage}{\textwidth}
\begin{lstlisting}[style=nonum]
/* empty heap: [ptr[2], ptr[3], ...] */
let a <- alloc<uint>; let b <- alloc<uint>; /* a <- ptr[2]; b <- ptr[3] */
let a -> alloc<uint>; let b -> alloc<uint>; /* a -> ptr[2]; b -> ptr[3] */
/* empty heap: [ptr[3], ptr[2], ...] */
\end{lstlisting}
\end{minipage}

\noindent
By deallocating \texttt{a} before \texttt{b}, the program reverses the position of the first two blocks of the free list. The state of the heap is semantically empty before and after the program executes, but these two memory representations are physically distinguishable.

\paragraph{Entanglement}
Effectively, the free list is \emph{entangled} with the program registers, even after the program deallocates all memory.
We call a quantum state entangled if it is not the a tensor product of two components~\citep{nielsen_chuang_2010}.
For example, the state $\frac{1}{2}{(\ket{00} + \ket{01} + \ket{10} + \ket{11})}$ is not entangled because it is the product of two copies of $\frac{1}{\sqrt{2}}{(\ket{0} + \ket{1})}$. By contrast, the \emph{Bell state}~\citep{bell} $\frac{1}{\sqrt{2}}{(\ket{00} + \ket{11})}$ is entangled because it cannot be written as the product of two qubits.

If $\ket{\ensuremath{\psi}}$ is separable into the states $\ket{\ensuremath{\psi}_A} \otimes \ket{\ensuremath{\psi}_B}$, then measuring the qubits of $\ket{\ensuremath{\psi}_A}$ deterministically leaves the remaining qubits in the state $\ket{\ensuremath{\psi}_B}$. By contrast, if $\ket{\ensuremath{\psi}}$ is entangled, then measuring a subset of its qubits leaves the remainder in a probabilistic mixture of states. For example, measuring one of the qubits in the entangled Bell state $\frac{1}{\sqrt{2}}{(\ket{00} + \ket{11})}$ results in the remaining qubit taking on a probabilistic mixture of states, $\ket{0}$ with probability $\frac{1}{2}$ and $\ket{1}$ with probability $\frac{1}{2}$ (\Cref{sec:background}).

In the example, the machine state cannot be written as a tensor product of the program registers and the empty heap.
An unintuitive consequence is that reclaiming the qRAM after a program finishes using it, which is equivalent to measuring it, would cause the program registers to probabilistically collapse to a mixture of classical states and corrupt the output of the program.

Thus, we next develop means by which Boson{} ensures that the entire heap, including all program-allocated data structures and the allocator's own free list metadata, is history-independent.

\subsection{Classical Address Randomization} \label{sec:randomization}

Classically, history independence is achieved through randomizing all addresses in a data structure. We define a \emph{statistical} formulation of history independence, adapted from~\citet{teague2001}:

\begin{definition}[Statistical History Independence]
    An abstract data structure implementation is \emph{statistically history independent} if and only if, when any two sequences of abstract operations yield equivalent data structures, then the distributions of their physical representations are identical.
\end{definition}

To choose new allocations uniformly at random, we initialize \texttt{hp} and the non-null addresses of the free list to a uniformly random permutation of $[1, \ldots, n]$.\footnotemark{} Doing so guarantees statistical history independence in the classical setting:
\footnotetext{Invoking randomness only at initialization means that an allocation immediately following a deallocation will yield the just-deallocated address. This correlation does not violate statistical history independence because the heap always remains in a uniformly random distribution over all possible choices of allocation sites.}

\begin{theorem}
    After any sequence of allocation and deallocation operations, the representation of the heap is statistically history-independent.
\end{theorem}

\begin{proof}
    Follows directly from Theorem 9 in~\citet{teague2001}.
\end{proof}

\subsection{Quantum Heap Symmetrization}

In the quantum setting, Boson{} achieves history independence through superposition, the analog of randomization.\footnote{Unlike classical probability distributions, quantum superposition states are on equal footing with basis states, and so we no longer need to distinguish strict and statistical history independence.}
It initializes \texttt{hp} and the non-null addresses of the free list to a uniform superposition of permutations via the following unitary operator, which we call \emph{symmetrization}:
\[
    \ket{1, \ldots, n} \mapsto \frac{1}{n!}\sum_{\pi \in S_{n}} \ket{\pi(1), \ldots, \pi(n)}
\]
This unitary operator is a central component of quantum simulation, in which it imposes bosonic exchange symmetry\footnote{Fermionic antisymmetry, which is closely related, additionally flips the sign according to the parity of the permutation $\pi$.}~\citep{Liboff1980IntroductoryQM} on the list. A multitude of implementations of this operator exist in the simulation literature, including~\citet{abrams1997} and~\citet{barenco1997}, who achieve implementations in $O(n^2 \log^2 n)$ gates; \citet{chiew2019}, in $O(n^2 \log n)$ gates; and~\citet{Berry2017ImprovedTF}, in $O(n \log n \log \log n)$ gates and parallel time $O(\log n \log \log n)$.\footnote{Comparable to the complexity of the quantum Fourier transform~\citep{qft}.} Boson{} performs this operation only once, before the program executes, to initialize the state of the heap.

\section{Related Work} \label{sec:related-work}

\paragraph{Quantum Programming with Data Structures}
The three requirements for quantum data structures were introduced by~\citet{ambainis2003} and elaborated by~\citet{bernstein2013}, who introduced radix trees~\citep{morrison} as a quantum implementation of sets, and~\citet{aaronson2019}. These authors also define quantum data structure operations such as creating a superposition of all sets.

\citet{Pechoux_2020} develop a quantum programming language with inductive data structures and recursion. Unlike Tower{}, its data structures are classical in structure, meaning that one may create a list of qubits but not create a superposition of lists of different length or perform operations over superpositions of lists, as is possible in Tower{} and necessary to implement a set data structure in superposition. Another distinction is that its programs may invoke measurement and are not necessarily reversible, whereas Tower{} programs denote unitary circuits.

\paragraph{Reversible Programming}

Janus~\citep{Lutz86,tokoyama2007} introduced reversible programming and conditions that are checked after an \texttt{if}-block completes. Consequent developments include \citet{thomsen2015,bowman2011,haulund2017}. Other applications include bidirectional lenses~\citep{bohannon2008} and reversible hardware~\citep{Vieri1995}.

\paragraph{Reversible Memory Management}
Uncomputation~\citep{bennett1989} has become a central feature of quantum programming languages such as~\citet{silq,qsharp,qiskit}. The fact that recursive uncomputation may lead to asymptotic slowdown was noted by~\citet{aaronson2002}. Proposed solutions include whole-program uncomputation~\citep{unqomp} and heuristics trading off between space and time~\citep{square}.

\citet{axelsen2013} present a reversible free list memory allocator, which inspired parts of Boson{} but is not history-independent.
\citet{buhrman2022} propose a quantum allocator that traverses a prefix tree stored in qRAM for every allocation. By contrast, Boson{} symmetrizes the heap once and then performs allocation in constant time.

\paragraph{History Independence}

\citet{teague2001} introduced history independence in the context of privacy and cryptography, in which it guarantees that an adversary with access to the physical memory of a system cannot recover sensitive information about the sequence of events that produced the current state. They present history-independent versions of hash tables and a general scheme for memory allocation that inspired parts of Boson{}. Later work~\citep{hartline,bajaj} elaborates the deterministic and statistical forms of history independence and provide additional schemes for history-independent data structure construction.

redpajama_set_name: RedPajamaArXiv