# Quantum Zeno-based Detection and State Engineering of Ultracold Polar
Molecules

Amit Jamadagni<EMAIL_ADDRESS>Institut für Theoretische
Physik, Leibniz Universität Hannover, Appelstraße 2, 30167 Hannover, Germany
Silke Ospelkaus  Institut für Quantenoptik, Leibniz Universität Hannover,
Welfengarten 1, 30167 Hannover, Germany  Luis Santos  Institut für
Theoretische Physik, Leibniz Universität Hannover, Appelstraße 2, 30167
Hannover, Germany  Hendrik Weimer  Institut für Theoretische Physik, Leibniz
Universität Hannover, Appelstraße 2, 30167 Hannover, Germany

###### Abstract

We present and analyze a toolbox for the controlled manipulation of ultracold
polar molecules, consisting of detection of molecules, atom-molecule
entanglement, and engineering of dissipative dynamics. Our setup is based on
fast chemical reactions between molecules and atoms leading to a quantum Zeno-
based collisional blockade in the system. We demonstrate that the experimental
parameters for achieving high fidelities can be found using a straightforward
numerical optimization. We exemplify our approach for a system comprised of
NaK molecules and Na atoms and we discuss the consequences of residual
imperfections such as a finite strength of the quantum Zeno blockade.

Ultracold polar molecules are very promising candidates for a wide range of
applications such as quantum simulation Moses2017  or searching for physics
beyond the Standard Model Tarbutt2013 . However, the lack of optical control
over the internal states due to the large number of vibrational levels
currently presents a severe obstacle towards realizing these applications.
Here, we show that strong chemical reactions between molecules and atoms
enable a dissipative interaction mechanism that in the quantum Zeno regime
allows to leverage the optical properties of atoms and achieve the same level
of control for the molecules.

In current experiments, ultracold molecules are photo-associated from laser
cooled atoms Ni2008 ; DeMarco2019  with full control over the final hyperfine
state Ospelkaus2010a . The resulting molecules can be manipulated by external
electric fields, microwave driving, or optical potentials, e.g., enabling to
load the molecules into an optical lattice Miranda2011 ; Reichsollner2017 .
Crucially, ultracold molecules can be subject to chemical reactions, both
between themselves as well as with their constituent atoms Ospelkaus2010 ;
Guo2018 . For some molecules such as NaK Park2015 ; Will2016 ; Seesselberg2018
, the chemical stability with respect to these atom-molecule reactions depends
on the atom species involved Zuchowski2010 .

In this Letter, we present a complete toolbox for transferring the optical
control over atoms to the realm of polar molecules. Our approach crucially
relies on the presence of strong chemical reactions between atoms and
molecules. In the quantum Zeno regime Zhu2014 , this dissipative atom-molecule
interaction implements a collisional blockade that allows for the efficient
detection of molecules, overcoming a longstanding challenge. In contrast to
previous proposals Covey2018 , our approach does not require high-fidelity
association and deassociation of the molecules. Furthermore, we demonstrate
how to extend our detection method to the generation of atom-molecule
entanglement and to the controlled dissipation of rotational excitations of
the molecules. We dicuss the expected fidelities for experimentally realistic
parameters, as well as the role of residual imperfections such as an imperfect
quantum Zeno blockade.

In the following, we will first discuss the basic mechanism to implement a
detection scheme for the molecules. Later on, we will show how this can be
generalized towards the generation of entanglement between the internal
degrees of freedom of a molecule and an atom. Finally, we will show how the
entangling operation can also be employed towards the controlled dissipation
of rotational excitations of the molecule, which can be readily used within
laser cooling protocols.

Figure 1: Quantum Zeno detection of molecules. (a) Bilayer setup of the system
with the atoms being in a Mott insulator state in the upper layer separated
from the molecules. (b) In the absence of a molecule in the neighboring site,
atoms can transfer from $\ket{L}$ to $\ket{R}$. (c) The presence of a molecule
inhibits the transfer to $\ket{R}$ due to a strong chemical reaction.

_Detection of molecules.—_ For the detection of the molecules, we consider a
bilayer setup of two two-dimensional optical lattice potentials, see Fig. 1.
Different layers for the atoms and molecules can be selected by magnetic and
electric field gradients, respectively, in combination with microwave fields.
Hence, it is possible to initially load all the Na atoms in one layer, while
the NaK molecules are located in the other layer. We assume that the tunneling
within the two lattice planes is strongly suppressed by the lattice
potentials, hence it is sufficient to consider a single double-well setup.
Additionally, we consider the atomic layer prepared in a Mott insulator state
with one atom per site. Owing to the differences in the AC polarizability
Holmgren2010 ; Neyenhuis2012 , as well as the fact that the atoms are much
lighter than the molecules, we limit the following analysis to the case where
only the atom moves with a hopping matrix element $J$, while the molecule
remains stationary throughout the process. The crucial dissipative element is
provided by a loss with a rate $\gamma$ induced by the chemical reaction
between Na atoms and NaK molecules Idziaszek2010 ; Ospelkaus2010 .

The central idea behind the detection mechanism is to attempt a Landau-Zener
transfer of the atom to the site potentially occupied by a molecule, e.g., by
adiabatically reversing the magnetic field gradient. If there is no molecule
on the second site, the transfer will succeed and the atom can be detected
using standard quantum gas microscope techniques Bakr2009 ; Sherson2010 ;
Haller2015 . However, in the presence of molecule in the second site, the
strong chemical reaction creates a quantum Zeno blockade Zhu2014  of the
Landau-Zener process. Hence, detecting the position of the atom after
completion of the Landau-Zener sweep allows to deduce the positions of the
molecules.

To be specific, we model the detection in terms of two independent Landau-
Zener processes, with and without the presence of a molecule on the second
site. For simplicity, we assume half filling of the molecular layer, i.e.,
equal probabilities for both processes, however the subsequent optimization
can also be tailored towards other molecular densities. Then, the probability
for a detection failure (either false positive or false negative) is simply
given by the averaged error probability of the two processes. We model the
Landau-Zener processes in terms of a non-Hermitian Hamiltonian

$H=\Delta(t)\sigma_{z}-J\sigma_{x}-\frac{i\gamma}{2}\mathopen{|}R\mathclose{\rangle}\mathopen{\langle}R\mathclose{|},$
(1)

where we have used Pauli matrices $\sigma_{\alpha}$ in the basis of the two
atom positons $\ket{L}$ and $\ket{R}$, while $\Delta(t)$ describes the
influence of the time-dependent magnetic field gradient. The dissipation
$\gamma$ vanishes in the absence of a molecule on the right site. The time-
dependent term $\Delta(t)$ is taken to be an odd polynomial in $t$ up to fifth
order, i.e., satisfying the constraints $\Delta(\pm\infty)=\pm\infty$ and
$\Delta(0)=0$. Then, we can minimize the total detection error $\varepsilon$
by optimizing the coefficients of the polynomial as well as the initial time
$t_{i}$, while the final time $t_{f}$ is given by $t_{f}=-t_{i}$. As shown in
Fig. 2, both Landau-Zener processes can be implemented with high success rate,
i.e., the total error $\varepsilon=0.03$ is low. We note that this error can
be even further reduced when starting from a high fidelity Mott insulator for
the atoms Bakr2011 , as observing no atom in either site clearly signals the
presence of a molecule.

Figure 2: Atom transfer probability for the atom in the presence ($p_{R}^{m}$)
or absence ($p_{R}^{\bar{m}}$) of the molecule. Additionally, the loss
$\varepsilon_{l}=1-p_{L}^{m}-p_{R}^{m}$ is shown ($\gamma=50\,J$).

_Atom-molecule entanglement.—_ As the next step, we extend the Zeno-based
detection scheme towards entanglement of the internal states of atoms and
molecules. The internal states $\ket{0}_{a/m}$ and $\ket{1}_{a/m}$ refer to
the rovibrational ground state and a rotationally excited state for the
molecule ($m$) and two hyperfine states of the atom ($a$), respectively. To
realize an entangling operation, we consider a setup consisting of three two-
dimensional planes, of which we again consider a single three well unit, see
Fig. 3a. We constrain the motion of the molecule (atom) to the left (right)
site and the center site, respectively. Additionally, we assume that the
motion takes only place within the $\ket{1}$ state of both atom and molecule.

A possible scheme to engineer these constrains may be as follows. In addition
to the time-dependent magnetic or electric field gradient, the central site
$\ket{C}$ may be shifted by an energy difference $\delta$ from that $\ket{L}$
and $\ket{R}$, such that direct hopping is prevented. Sites $\ket{L}$ and
$\ket{C}$ ($\ket{R}$ and $\ket{C}$) are connected along the $x$ ($y$)
direction. A first Raman pair (or rf frequency) with frequency transfer
$\Delta\omega_{1}=\Delta$, Rabi frequency $\Omega_{1}$, and momentum transfer
$\vec{\Delta}k_{1}=\Delta k_{1}\vec{e}_{x}$, induces a molecular hopping rate
$J_{m}=\hbar\Omega_{1}\langle 1,L|_{m}e^{i\Delta k_{1}x}|1,C\rangle_{m}$.
Crucially, $\langle 1,R|_{m}e^{i\Delta k_{1}x}|1,C\rangle_{m}=0$ due to
orthogonality of the Wannier-like functions characterizing each lattice site.
As a result, molecules in the $|1\rangle_{m}$ state only hop from $\ket{L}$ to
$\ket{C}$. Similarly, using a second Raman pair with
$\Delta\omega_{2}=\Delta$, $\Omega_{2}$, and $\vec{\Delta}k_{2}=\Delta
k_{2}\vec{e}_{y}$, we may induce a hopping rate $J_{a}=\hbar\Omega_{2}\langle
1,R|_{a}e^{i\Delta k_{2}y}|1,C\rangle_{a}$, for atoms between $\ket{R}$ and
$\ket{C}$ without any atomic hopping from $\ket{C}$ to $\ket{L}$.

Figure 3: Atom-molecule entanglement. (a) Three-well setup for the system with
a central reaction site $\ket{C}$, while molecule and atom start in $\ket{L}$
and $\ket{R}$, respectively. (b) Matrix representation of the optimized
process, realizing a CZ gate with high fidelity ($\gamma=50\,J$).

The Hamiltonian of the three-well setup is of the form

$\displaystyle H$
$\displaystyle=B\mathopen{|}1\mathclose{\rangle}\mathopen{\langle}1\mathclose{|}_{m}+E_{HFS}\mathopen{|}1\mathclose{\rangle}\mathopen{\langle}1\mathclose{|}_{a}+\Delta_{m}(t)\mathopen{|}L\mathclose{\rangle}\mathopen{\langle}L\mathclose{|}_{m}$
$\displaystyle+\Delta_{a}(t)\mathopen{|}R\mathclose{\rangle}\mathopen{\langle}R\mathclose{|}_{a}-\frac{i\gamma}{2}\mathopen{|}C\mathclose{\rangle}\mathopen{\langle}C\mathclose{|}_{m}\otimes\mathopen{|}C\mathclose{\rangle}\mathopen{\langle}C\mathclose{|}_{a}$
$\displaystyle-(J_{m}\mathopen{|}1,L\mathclose{\rangle}\mathopen{\langle}1,C\mathclose{|}_{m}+J_{a}\mathopen{|}1,R\mathclose{\rangle}\mathopen{\langle}1,C\mathclose{|}_{a}+\text{H.c}),$
(2)

where $B$ is the rotational constant of the molecule, $E_{HFS}$ is the
hyperfine splitting of the atom and $\Delta_{m/a}$ refers to the electric and
magnetic field gradients, respectively. For simplicity, we assume the
condition $\Delta_{m}(t)=-\Delta_{a}(t)\equiv\Delta(t)$, although this choice
is not essential for achieving high fidelity entanglement.

The entangling operation we are realizing corresponds to a Controlled-Z (CZ)
quantum gate for the internal states. We restrict the computational states to
the molecule being in the motional state $\ket{L}$ and the atom being in
$\ket{R}$, i.e., any residual occupation of the central site constitutes a
gate error. Without loss of generality, we set the tunnelling matrix elements
to be identical, i.e., $J_{a}=J_{m}\equiv J$. The CZ gate is implemented using
a similar Landau-Zener protocol as our detection scheme, however the
constraints on $\Delta(t)$ are different. Since the motional degrees of
freedom need to return to the initial value at the end of the gate, this
requires $\Delta(t)=\Delta(-t)$, therefore we take $\Delta(t)$ to be an even
polynomial in $t$ up to fourth order. Then, optimizing the coefficients of the
polynomial as well as the gate time result in a close approximation to an
exact CZ gate, see Fig. 3b. To capture the performance of the gate in a single
number, we use the fidelity $F=|\braket{\psi_{+}}{\psi(t_{f})}|^{2}$ to create
the maximally entangled state
$\ket{\psi_{+}}=\frac{1}{\sqrt{2}}(\ket{0L_{m}0R_{a}}+\ket{1L_{m}1R_{a}})$, as
this constitutes a worst case scenario for a large class of error mechanisms
Weimer2012 . For a dissipation strength of $\gamma=50\,J$, we can achieve a
fidelity of $F=0.913$, which approaches a regime that is sufficient for the
digital quantum simulation of important many-body spin models Weimer2013a .
Finally, we would like to note that the presented atom-molecule entanglement
can be readily converted into molecule-molecule entanglement using standard
entanglement transfer protocols Barenco1995 .

In the previous analyses, we have assumed that the loss rate $\gamma=50\,J$ is
fixed with respect to the tunnelling matrix element. However, by tuning the
laser parameters for generating the potential wells, it is possible to make
this ratio highly tunable. Therefore, it is interesting to investigate how our
protocols responds to such a change, it particular there might be practical
limitations on how low $J$ can become before other error mechanisms such as
thermal losses, buffer gas collisions, etc. kick in. Figure 4 shows that both
the detection and the entanglement error $\varepsilon=1-F$ both follow the
expected $1/\gamma$ quantum Zeno profile, with the detection error being
slightly below the entanglement error.

Figure 4: Errors $\varepsilon$ for the detection and entangling process as a
function of $\gamma/J$. Both curves follow a quantum Zeno profile proportional
to $J/\gamma$.

_Dissipative quantum state engineering.—_ Let us now extend the mechanism
behind the CZ gate towards the controlled dissipation of rotational
excitations. For polar molecules, such a mechanism cannot reliably be realized
using optical pumping due to the large number of vibrational levels an optical
excitation can decay into. Nevertheless, such a controlled dissipation channel
has immediate application for the laser cooling of molecules Zhao2012 , as
well as for the dissipative engineering of tailored quantum many-body states
Diehl2008 ; Verstraete2009 ; Weimer2010 .

To realize this dissipative state engineering, we consider two different
strategies. The first strategy is to apply a pulsed scheme, in which the CZ
gate $U_{CZ}$ is combined with single qubit gates in both the atom and the
molecule, in close analogy to a digital quantum simulator. We consider the
gate sequence

$U=U_{CZ}R_{x}^{(a)}(\phi)U_{H}^{(m)}U_{CZ}U_{H}^{(m)}R_{x}^{(a)}(\phi),$ (3)

where $R_{x}(\phi)=\exp(i\phi\sigma_{x})$ is the single qubit rotation about
the $x$ axis and $U_{H}$ is the Hadamard gate. After the gate sequence, the
molecule and the atom will be entangled. However, a subsequent optical pumping
of the atom according to $\ket{1}\to\ket{0}$ realizes a discrete quantum
master equation in Lindblad form according to

$\rho_{m}^{\prime}=\rho_{m}+\phi^{2}\sigma_{-}^{(m)}\rho_{m}\sigma_{+}^{(m)}-\frac{\phi^{2}}{2}\left\\{\sigma_{+}^{(m)}\sigma_{-}^{(m)},\rho_{m}\right\\}+O(\phi^{4}).$
(4)

This dissipative dynamics can then be interspersed with coherent driving of
the rotational states of the molecules to achieve the desired quantum state
engineering.

The second strategy for this dissipative state engineering uses a continuous
driving of both the molecular and the atomic transitions rather than a pulsed
quantum gate sequence. This has two advantages. On the one hand, the mechanism
behind the CZ gate can be understood to implement an effective
$\sigma_{z}^{(m)}\sigma_{z}^{(a)}$ interaction, which cannot transfer energy
from the molecule to the atom. By going into the rotating frame of the
driving, this is converted into a $\sigma_{x}^{(m)}\sigma_{x}^{(a)}$
interaction, which contains terms that lead to an energy transfer. The second
advantage is that the energy difference between the rotational constant $B$
and the hyperfine splitting $E_{HFS}$ is too large to observe direct energy
transfer from the molecule to the atom. In the rotating frame, however, this
large energy difference is converted into the energy difference involving the
respective detunings and Rabi frequencies of the driving. When the differences
in the detunings and the Rabi frequencies vanish, efficient energy transfer
becomes possible under a condition very similar to the Hartmann-Hahn driving
in nuclear magnetic resonance Hartmann1962 . In this case, the Hamiltonian is
given by

$\begin{split}H=&-J(\mathopen{|}1,L\mathclose{\rangle}\mathopen{\langle}1,C\mathclose{|}_{m}+\mathopen{|}1,R\mathclose{\rangle}\mathopen{\langle}1,C\mathclose{|}_{a}+\text{H.c.})\\\
&+\Omega(\sigma_{x}^{(m)}+\sigma_{x}^{(a)})+\delta(\sigma_{z}^{(m)}+\sigma_{z}^{(a)})\\\
&-\Delta\mathopen{|}L\mathclose{\rangle}\mathopen{\langle}L\mathclose{|}-\Delta\mathopen{|}R\mathclose{\rangle}\mathopen{\langle}R\mathclose{|},\end{split}$
(5)

where $\Omega$ is the Rabi frequency and $\delta$ is the detuning used both
for the driving of the molecule and the atom. Addionally, we consider optical
pumping of the atom by including a quantum jump operator
$c_{\kappa}=\sqrt{\kappa}\sigma_{-}^{(a)}$ in the quantum master equation
describing the dynamics,

$\frac{d}{dt}\rho=-\frac{i}{\hbar}[H,\rho]+\sum\limits_{i=\gamma,\kappa}\left(c_{i}\rho
c_{i}^{\dagger}-\frac{1}{2}\left\\{c_{i}^{\dagger}c_{i},\rho\right\\}\right).$
(6)

Here, the jump operator $c_{\gamma}$ describes the occurence of a chemical
reation, which removes both the atom and the molecule from the system. We then
optimize the set of parameters $(\Omega,\delta,\Delta,\kappa)$ such that an
initial state of $\ket{1}_{m}\ket{0}_{a}$ goes to $\ket{0}_{m}\ket{0}_{a}$.
Figure 5 shows that this optimization leads to the initial rotational
excitation being dissipated with high probability, while the loss resulting
from chemical reaction remains low. We would like to note that this continuous
dissipative process might be experimentally easier to realize than a pulsed
sequence, however coming at the expense of requiring longer preparation times.
We checked the robustness of our protocol with respect to an imperfect
experimental implementation of the optimized parameters. Upon decreasing the
atomic Rabi frequency by $10\%$ compared to its optimal value, we observe that
the final probability to reach the $\ket{0}_{m}\ket{0}a$ state decreses by
merely $2\%$. This underlines the robustness of our optimization protocol.

Figure 5: Dissipation of a rotational excitation. The probability to find the
molecule in the rotationally excited state $\ket{1}$, $p_{1}^{(m)}$ closely
follows an exponential decay, while the ground state probability $p_{0}^{(m)}$
increases in a similar way. The inset shows that the overall loss from the
chemical reaction remains low ($\gamma=50\,J$).

_Experimental parameters.—_ In the following, we will calculate the loss
coefficient $\gamma$ for the exothermic reaction
$\text{NaK}+\text{Na}\to\text{Na}_{2}+\text{K}$. The $\text{NaK}+\text{Na}$
system has a van der Waals coefficient of $C_{6}=3592\,\text{a.u.}$
Zuchowski2013 , from which we can calculate the universal rate coefficient
$\beta$ of the chemical reaction Idziaszek2010 , which is given by

$\beta=\frac{2\hbar^{3/2}\Gamma(1/4)^{2}}{(2\mu^{5}C_{6})^{1/4}}=1.47\times
10^{-10}\,\text{cm}^{3}\,\text{s}^{-1},$ (7)

where $\mu$ is the reduced mass. In a potential well corresponding to an
oscillator length of $a_{0}=100\,\text{nm}$, this will result in a reaction
rate of $\gamma=50\,\text{kHz}$. Compared to the typical tunnelling matrix
element of $J\sim 100\text{--}1000\,\text{Hz}$ Bloch2008 , dissipation rates
$\gamma=50\text{--}500\,J$ deep in the quantum Zeno regime can be achieved.

In summary, we have presented a toolbox for the controlled manipulation of
ultracold polar molecules via dissipative interactions with atoms. Our results
pave the way for important experimental advances in the detection,
entanglement, and dissipative quantum state preparation of molecular quantum
many-body systems. While we have exemplified our approach for NaK, it can also
be readily applied to other molecules, provided there is at least one
exothermic reaction with one of its constituent atoms. An interesting question
for future work is whether the dynamics leading to the formation of ultracold
collision complexes Mayle2012  can be harnessed for coherent manipulation of
molecules in a similar way.

###### Acknowledgements.

This work was funded by the Volkswagen Foundation and the DFG within SFB 1227
(DQ-mat, projects A03 and A04) and under Germany’s Excellence Strategy
EXC-2123-A2 (QuantumFrontiers).

## References

  * (1) S. A. Moses, J. P. Covey, M. T. Miecnikowski, D. S. Jin, and J. Ye,  New frontiers for quantum gases of polar molecules,  Nature Phys. 13, 13 (2017).
  * (2) M. R. Tarbutt, B. E. Sauer, J. J. Hudson, and E. A. Hinds,  Design for a fountain of YbF molecules to measure the electron’s electric dipole moment,  New J. Phys. 15, 053034 (2013).
  * (3) K.-K. Ni, S. Ospelkaus, M. H. G. de Miranda, A. Pe’er, B. Neyenhuis, J. J. Zirbel, S. Kotochigova, P. S. Julienne, D. S. Jin, and J. Ye,  A High Phase-Space-Density Gas of Polar Molecules,  Science 322, 231 (2008).
  * (4) L. De Marco, G. Valtolina, K. Matsuda, W. G. Tobias, J. P. Covey, and J. Ye,  A degenerate Fermi gas of polar molecules,  Science 363, 853 (2019).
  * (5) S. Ospelkaus, K.-K. Ni, G. Quéméner, B. Neyenhuis, D. Wang, M. H. G. de Miranda, J. L. Bohn, J. Ye, and D. S. Jin,  Controlling the Hyperfine State of Rovibronic Ground-State Polar Molecules,  Phys. Rev. Lett. 104, 030402 (2010).
  * (6) M. H. G. de Miranda, A. Chotia, B. Neyenhuis, D. Wang, G. Quemener, S. Ospelkaus, J. L. Bohn, J. Ye, and D. S. Jin,  Controlling the quantum stereodynamics of ultracold bimolecular reactions,  Nature Phys. 7, 502 (2011).
  * (7) L. Reichsöllner, A. Schindewolf, T. Takekoshi, R. Grimm, and H.-C. Nägerl,  Quantum Engineering of a Low-Entropy Gas of Heteronuclear Bosonic Molecules in an Optical Lattice,  Phys. Rev. Lett. 118, 073201 (2017).
  * (8) S. Ospelkaus, K.-K. Ni, D. Wang, M. H. G. de Miranda, B. Neyenhuis, G. Quéméner, P. S. Julienne, J. L. Bohn, D. S. Jin, and J. Ye,  Quantum-State Controlled Chemical Reactions of Ultracold Potassium-Rubidium Molecules,  Science 327, 853 (2010).
  * (9) M. Guo, X. Ye, J. He, M. L. González-Martínez, R. Vexiau, G. Quéméner, and D. Wang,  Dipolar Collisions of Ultracold Ground-State Bosonic Molecules,  Phys. Rev. X 8, 041044 (2018).
  * (10) J. W. Park, S. A. Will, and M. W. Zwierlein,  Ultracold Dipolar Gas of Fermionic ${}^{23}\mathrm{Na}^{40}\mathrm{K}$ Molecules in Their Absolute Ground State,  Phys. Rev. Lett. 114, 205302 (2015).
  * (11) S. A. Will, J. W. Park, Z. Z. Yan, H. Loh, and M. W. Zwierlein,  Coherent Microwave Control of Ultracold ${}^{23}\mathrm{Na}^{40}\mathrm{K}$ Molecules,  Phys. Rev. Lett. 116, 225306 (2016).
  * (12) F. Seeßelberg, X.-Y. Luo, M. Li, R. Bause, S. Kotochigova, I. Bloch, and C. Gohle,  Extending Rotational Coherence of Interacting Polar molecules in a Spin-Decoupled Magic Trap,  Phys. Rev. Lett. 121, 253401 (2018).
  * (13) P. S. Żuchowski and J. M. Hutson,  Reactions of ultracold alkali-metal dimers,  Phys. Rev. A 81, 060703 (2010).
  * (14) B. Zhu, B. Gadway, M. Foss-Feig, J. Schachenmayer, M. L. Wall, K. R. A. Hazzard, B. Yan, S. A. Moses, J. P. Covey, D. S. Jin, J. Ye, M. Holland, and A. M. Rey,  Suppressing the Loss of Ultracold Molecules Via the Continuous Quantum Zeno Effect,  Phys. Rev. Lett. 112, 070404 (2014).
  * (15) J. P. Covey, L. D. Marco, Ó. L. Acevedo, A. M. Rey, and J. Ye,  An approach to spin-resolved molecular gas microscopy,  New J. Phys. 20, 043031 (2018).
  * (16) W. F. Holmgren, M. C. Revelle, V. P. A. Lonij, and A. D. Cronin,  Absolute and ratio measurements of the polarizability of Na, K, and Rb with an atom interferometer,  Phys. Rev. A 81, 053607 (2010).
  * (17) B. Neyenhuis, B. Yan, S. A. Moses, J. P. Covey, A. Chotia, A. Petrov, S. Kotochigova, J. Ye, and D. S. Jin,  Anisotropic Polarizability of Ultracold Polar ${}^{40}\mathrm{K}^{87}\mathrm{Rb}$ Molecules,  Phys. Rev. Lett. 109, 230403 (2012).
  * (18) Z. Idziaszek and P. S. Julienne,  Universal Rate Constants for Reactive Collisions of Ultracold Molecules,  Phys. Rev. Lett. 104, 113202 (2010).
  * (19) W. S. Bakr, J. I. Gillen, A. Peng, S. Fölling, and M. Greiner,  A quantum gas microscope for detecting single atoms in a Hubbard-regime optical lattice,  Nature (London)462, 74 (2009).
  * (20) J. F. Sherson, C. Weitenberg, M. Endres, M. Cheneau, I. Bloch, and S. Kuhr,  Single-atom-resolved fluorescence imaging of an atomic Mott insulator,  Nature 467, 68 (2010).
  * (21) E. Haller, J. Hudson, A. Kelly, D. A. Cotta, B. Peaudecerf, G. D. Bruce, and S. Kuhr,  Single-atom imaging of fermions in a quantum-gas microscope,  Nature Physics 11, 738 (2015).
  * (22) W. S. Bakr, P. M. Preiss, M. E. Tai, R. Ma, J. Simon, and M. Greiner,  Orbital excitation blockade and algorithmic cooling in quantum gases,  Nature (London)480, 500 (2011).
  * (23) H. Weimer, N. Y. Yao, C. R. Laumann, and M. D. Lukin,  Long-Range Quantum Gates using Dipolar Crystals,  Phys. Rev. Lett. 108, 100501 (2012).
  * (24) H. Weimer,  Quantum simulation of many-body spin interactions with ultracold polar molecules,  Mol. Phys. 111, 1753 (2013).
  * (25) A. Barenco, C. H. Bennett, R. Cleve, D. P. DiVincenzo, N. Margolus, P. Shor, T. Sleator, J. A. Smolin, and H. Weinfurter,  Elementary gates for quantum computation,  Phys. Rev. A 52, 3457 (1995).
  * (26) B. Zhao, A. W. Glaetzle, G. Pupillo, and P. Zoller,  Atomic Rydberg Reservoirs for Polar Molecules,  Phys. Rev. Lett. 108, 193007 (2012).
  * (27) S. Diehl, A. Micheli, A. Kantian, B. Kraus, H. P. Büchler, and P. Zoller,  Quantum states and phases in driven open quantum systems with cold atoms,  Nature Phys. 4, 878 (2008).
  * (28) F. Verstraete, M. M. Wolf, and J. Ignacio Cirac,  Quantum computation and quantum-state engineering driven by dissipation,  Nature Phys. 5, 633 (2009).
  * (29) H. Weimer, M. Müller, I. Lesanovsky, P. Zoller, and H. P. Büchler,  A Rydberg quantum simulator,  Nature Phys. 6, 382 (2010).
  * (30) S. R. Hartmann and E. L. Hahn,  Nuclear Double Resonance in the Rotating Frame,  Phys. Rev. 128, 2042 (1962).
  * (31) P. S. Żuchowski, M. Kosicki, M. Kodrycka, and P. Soldán,  van der Waals coefficients for systems with ultracold polar alkali-metal molecules,  Phys. Rev. A 87, 022706 (2013).
  * (32) I. Bloch, J. Dalibard, and W. Zwerger,  Many-body physics with ultracold gases,  Rev. Mod. Phys. 80, 885 (2008).
  * (33) M. Mayle, B. P. Ruzic, and J. L. Bohn,  Statistical aspects of ultracold resonant scattering,  Phys. Rev. A 85, 062712 (2012).


<concept_desc>Software and its engineering Software verification</concept_desc>

[500]Software and its engineering General programming languages

]Refinement Reflection: Complete Verification with SMT

Niki Vazou

University of Maryland

Anish Tondwalkar

University of California, San Diego

Vikraman Choudhury

Indiana University

Ryan G. Scott

Indiana University

Ryan R. Newton

Indiana University

Philip Wadler

University of Edinburgh and Input Output HK

Ranjit Jhala

University of California, San Diego

<concept_desc>Software and its engineering Software verification</concept_desc>

[500]Software and its engineering General programming languages

We introduce Refinement Reflection,
a new framework for building SMT-based
deductive verifiers.

The key idea is to reflect the code
implementing a user-defined function
into the function's (output) refinement
As a consequence, at uses of
the function, the function definition
is instantiated in the SMT logic in a precise fashion
that permits decidable verification.

Reflection allows the user to write
equational proofs of programs
just by writing other programs
using pattern-matching
and recursion to perform case-splitting
and induction.
Thus, via the propositions-as-types principle,
we show that reflection permits the
specification of arbitrary
functional correctness properties.

Finally, we introduce a proof-search algorithm called
Proof by Logical Evaluation
that uses techniques from model
checking and abstract interpretation,
to completely automate equational

We have implemented reflection in
and used it to verify that
the widely used instances of the Monoid,
Applicative, Functor, and Monad typeclasses
actually satisfy key algebraic laws
required to make the clients safe,
and have used reflection to build the first
library that actually verifies assumptions
about associativity and ordering that are
crucial for safe deterministic parallelism.

§ INTRODUCTION

Deductive verifiers fall roughly
into two camps.

Satisfiability Modulo Theory (SMT)
based verifiers (and )
use fast decision procedures to
automate the verification of programs that
only require reasoning over a fixed
set of theories like linear arithmetic,
string, set and bitvector operations.

These verifiers, however, encode the
semantics of user-defined functions
with universally-quantified axioms
and use incomplete (albeit effective)
heuristics to instantiate those axioms.

These heuristics make it difficult to
characterize the kinds of proofs that
can be automated, and hence,
explain why a given proof attempt
fails <cit.>.

At the other end, we have
Type-Theory (TT) based theorem provers
(and )
that use type-level computation
(normalization) to facilitate
principled reasoning about
terminating user-defined functions,
but which

require the user to supply
lemmas or rewrite hints

to discharge proofs
over decidable theories.

We introduce Refinement Reflection,
a new framework for building SMT-based
deductive verifiers, which permits the
specification of arbitrary properties
and yet enables complete, automated
SMT-based reasoning about user-defined

In previous work, refinement types
<cit.> — which decorate
basic types ("Integer") with SMT-decidable
predicates ("v:Integer | 0 <= v        v < 100") — were
used to retrofit so-called shallow
verification, such as array bounds checking, into
several languages:

ML <cit.>,
C <cit.>,
Haskell <cit.>,
TypeScript <cit.>, and
Racket <cit.>.

In this work,
we extend refinement types with refinement reflection,
leading to the following three contributions.

1. Refinement Reflection

Our first contribution is the notion of
refinement reflection.

To reason about user-defined functions,
the function's implementation is
reflected into its (output)
refinement-type specification,
thus converting the function's
type signature into a precise
description of the function's behavior.

This simple idea has a profound consequence:
at uses of the function, the standard
rule for (dependent) function application
yields a precise means of reasoning about
the function ( <ref>).

2. Complete Specification

Our second contribution is a
library of combinators
that lets programmers compose
sophisticated proofs
from basic refinements and
function definitions.

Our proof combinators let programmers
use existing language mechanisms, like
branches (to encode case splits),
recursion (to encode induction), and
functions (to encode auxiliary lemmas),
to write proofs that look very much like

their pencil-and-paper
analogues ( <ref>).

Furthermore, since proofs are literally
just programs, we use the principle of
propositions-as-types <cit.>
(known as the Curry-Howard isomorphism <cit.>)
to show

that SMT-based verifiers can
express any natural deduction proof,
thus providing a pleasant
implementation of
natural deduction
that can be used for
pedagogical purposes ( <ref>).

3. Complete Verification

While equational proofs can be very and expressive, writing them out can
quickly get exhausting.

Our third contribution is
Proof by Logical Evaluation ()
a new proof-search algorithm
that automates

equational reasoning.

The key idea in is to mimic
type-level computation within SMT-logics
by representing functions in a
guarded form <cit.>
and repeatedly unfolding function application
terms by instantiating them with their definition
corresponding to an enabled guard.

We formalize a notion of equational proof
and show that the above strategy is
complete: it is guaranteed
to find an equational proof if one exists.

Furthermore, using techniques from
the literature on Abstract
Interpretation <cit.>
and Model Checking <cit.>,
we show that the above proof search
corresponds to a universal
(or must) abstraction of
the concrete semantics of the
user-defined functions.

Thus, since those functions are total,

we obtain the pleasing
guarantee that proof search
terminates ( <ref>).

We evaluate our approach by implementing
refinement reflection and in
<cit.>, thereby
turning Haskell into a theorem prover.

Repurposing an existing programming language allows us
to take advantage of a mature compiler and an ecosystem of
libraries, while keeping proofs and programs in the same

We demonstrate the benefits of this
conversion by proving typeclass laws.

Haskell's typeclass machinery has led
to a suite of expressive abstractions
and optimizations which, for correctness,
crucially require typeclass instances
to obey key algebraic laws.

We show how reflection and can be used to verify that widely
used instances of the Monoid,
Applicative, Functor, and Monad
typeclasses satisfy the respective

Finally, we use reflection to
create the first deterministic
parallelism library that actually
verifies assumptions about
associativity and ordering
that ensure determinism ( <ref>).

Thus, our results demonstrate
that Refinement Reflection and
Proof by Logical Evaluation
identify a new design for
deductive verifiers which,
by combining the complementary
strengths of SMT- and TT- based
approaches, enables complete
verification of expressive
specifications spanning
decidable theories and
user defined functions.

§ OVERVIEW

We start with an overview of how SMT-based refinement
reflection lets us write proofs as plain
functions and how automates equational reasoning.

§.§ Refinement Types

First, we recall some preliminaries about specification
and verification with refinement types.

Refinement types are the source program's (here
Haskell's) types refined with logical predicates drawn
from an SMT-decidable logic <cit.>.

For example, we define "Nat" as the set of "Integer" values
"v" that satisfy the predicate "0 <= v" from
the quantifier-free logic of linear arithmetic and
uninterpreted functions (QF-UFLIA <cit.>):

type Nat =  v:Integer | 0 <= v

Specification & Verification

Throughout this section,
to demonstrate the proof features we add to ,
we will use the textbook Fibonacci function which we type as follows.

fib :: Nat -> Nat
fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

To ensure termination, the input type's
refinement specifies a pre-condition
that the parameter must be "Nat".
The output type's refinement specifies
a post-condition that the result
is also a "Nat".

Refinement type checking automatically
verifies that if "fib" is invoked with
a non-negative "Integer", then it terminates
and yields a non-negative "Integer".

We define a data type representing propositions
as an alias for unit:

type $\typp$ = ()

Prop is also in HOL, and it's encoded
as Bool, so this might be confusing,
maybe this should be Proof instead?

which can be refined with propositions about
the code, that $2 + 2$ equals $4$

type Plus_2_2 =  v: $\typp$ | 2 + 2 = 4

For simplicity, in , we abbreviate the above
to "type Plus_2_2 =  2 + 2 = 4 ".

Universal & Existential Propositions

Using the standard encoding of <cit.>,
known as the Curry-Howard isomorphism,
refinements encode universally-quantified propositions as
dependent function types of the form:

type Plus_comm = x:Integer -> y:Integer ->  x + y = y + x

As "x" and "y" refer to arbitrary inputs,
any inhabitant of the above type is a proof
that "Integer" addition commutes.

Refinements encode existential quantification via
dependent pairs of the form:

type Int_up = n:Integer -> (m::Integer, n < m)

The notation "(m :: t, t')" describes dependent pairs
where the name "m" of the first element can appear
inside refinements of the second element.

Thus, "Int_up" states the proposition that for
every integer "n", there exists
one that is larger than "n".

While quantifiers cannot appear directly
inside the refinements, dependent functions and
pairs allow us to specify quantified propositions.

One limitation of this encoding is that quantifiers
cannot exist inside refinement's logical connectives (like $\land$ and $\lor$).

In  <ref>, we describe how to
encode logical connectives using data types,
conjunction as a product and disjunction as
a union, how to specify arbitrary,
quantified propositions
using refinement types, have complete specifications,
and how to verify those propositions using refinement
type checking.

We prove the above propositions by
writing Haskell programs, for example

plus_2_2 :: Plus_2_2        plus_comm :: Plus_comm        int_up :: Int_up
plus_2_2 = ()               plus_comm = y -> ()        int_up = -> (n+1,())

Standard refinement typing reduces the above to
the respective verification conditions (VCs)

$$ \ttrue \Rightarrow 2 + 2 = 4 \quad \quad \quad
\forall \ x,\ y\ .\ \ttrue \Rightarrow x + y = y + x \quad \quad \quad
\forall \ n\ . n < n+1 $$

which are easily deemed valid by the SMT solver, allowing us
to prove the respective propositions.

Soundness and Lazy Evaluation

Readers familiar with Haskell's lazy
semantics may be concerned that “bottom”,
which inhabits all types, makes our proofs suspect.

Fortunately, as described in <cit.>, ,
by default, checks that user defined functions
provably terminate and are total (return non-bottom values,
and do not throw any exceptions),
which makes our proofs sound.

checks that each function is terminating using
a termination metric
a natural number that decreases at each recursive call.

For instance, if we generalize the signature
of "fib" to "Integers", as shown below, then
reports a termination error:

fib :: n:Integer -> Integer

generates a type error in the definition of "fib" since in
the recursive calls "fib (n-1)" and "fib (n-2)"
the arguments "n-1" and "n-2"
cannot be proved to be non-negative and less than "n".

Both these proof obligations are satisfied when
the domain of "fib" is restricted to natural numbers.

fib :: n:Nat -> Nat / [n]

The above type signature is explicitly annotated
with the user specified termination metric "/ [n]"
declaring that "n" is the decreasing natural number.

heuristically assumes that the termination metric
is always the first argument of the function (that can be mapped to natural numbers),
thus, the above explicit termination metric can be omitted.

Not all Haskell functions terminate.

The "lazy" annotation
deactivates termination
checking, for the
the "diverge" function
shown below.

Haskell terms marked as "lazy"
could unsoundly be used
as proof terms, much like 's
unsoundness with respect to "Admitted".

For example, the following is
accepted by

lazy diverge
diverge :: x:Integer ->  x = 0
diverge x = diverge x

Totality Checking
further checks that all user-specified functions are totally defined.
For instance the below definition

fibPartial 0 = 0
fibPartial 1 = 1

generates a totality error.

The above definition is completed, by GHC,
with an "error" invocation

fibPartial 0 = 0
fibPartial 1 = 1
fibPartial _ = error "undefined"

Thus, to check totality, simply ascribes the precondition "false" to "error"

error ::  v:String | false  -> a

Thus, to typecheck "fibPartial", needs to prove that the call to "error"
is dead-code, happens under an inconsistent environment. As this check fails,
generates a totality error.

As with termination checking,
provides an unsound
error function "unsoundError" with no false precondition.

In the sequel (and in our evaluation)
we assume that proof terms are generated without
any unsound uses of "lazy" or "unsafeError".

However, note that lazy, diverging functions
can be soundly verified, and diverging code
can soundly co-exist with terminating proof
terms: we refer the reader to <cit.> for details.

§.§ Refinement Reflection

Suppose we wish to prove properties about the "fib"
function, that "fib 2 = 1".

Standard refinement type checking runs into two problems.

First, for decidability and soundness, arbitrary
user-defined functions cannot belong in the refinement
logic, we cannot refer to "fib" in a refinement.

Second, the only specification that a refinement type checker
has about "fib" is its type "Nat -> Nat" which is
too weak to verify "fib 2 = 1".

To address both problems, we "reflect fib" into the
logic which sets the three steps of refinement
reflection in motion.

Step 1: Definition

The annotation creates an uninterpreted function
"!fib! :: Integer -> Integer" in the refinement logic.

By uninterpreted, we mean that the logical "!fib!"
is not connected to the program function
"fib"; in the logic, "!fib!" only satisfies the
congruence axiom

$\forall n, m.\ n = m\ \Rightarrow\ \fib{n} = \fib{m}$.

On its own, the uninterpreted function is
not terribly useful: we cannot check "!fib! 2 = 1"
as the SMT solver cannot prove the
$\ttrue \Rightarrow \fib{2} = 1$
which requires reasoning about "fib"'s

Step 2: Reflection

In the next key step, we reflect the definition
of "fib" into its refinement type by automatically
strengthening the user defined type for "fib" to:

fib :: n:Nat ->  v:Nat | v = !fib! n        fibP n

where "fibP" is an alias for a refinement
automatically derived from the
function's definition:

fibP n $\doteq$ n == 0 $\Rightarrow$ !fib! n = 0
$\wedge$ n == 1 $\Rightarrow$ !fib! n = 1
$\wedge$ n  > 1 $\Rightarrow$ !fib n! = !fib! (n-1) + !fib! (n-2)

Step 3: Application

With the reflected refinement
type, each application of "fib"
in the code automatically
unfolds the definition
of "fib" once in the logic.

We prove "!fib! 2 = 1" by:

pf_fib2 ::  !fib! 2 = 1
pf_fib2 = let  t0 = #fib# 0; t1 = #fib# 1; t2 = #fib# 2  in ()

We write in bold red, "#f#", to highlight places where the
unfolding of "f"'s definition is important.

Via refinement typing, the above yields the
following VC that is discharged by SMT, even
though "!fib!" is uninterpreted:

$$(\fibdef\ 0 \ \wedge\ \fibdef\ 1 \ \wedge\ \fibdef\ 2) \  \Rightarrow\ (\fib{2} = 1)$$

The verification of "pf_fib2" relies
merely on the fact that "fib" is applied
to (unfolded at) "0", "1", and "2".

The SMT solver automatically combines
the facts, once they are in the antecedent.
Thus, the following is also verified:

pf_fib2' :: v:[Nat] | !fib! 2 = 1
pf_fib2' = [ #fib# 0, #fib# 1, #fib# 2 ]

In the next subsection, we will continue to use explicit,
step-by-step proofs as above, but we will introduce tools
for proof composition.

Then, in  <ref> we will show how to
eliminate unnecessary details from such proofs, using
Proof by Logical Evaluation ().

§.§ Equational Proofs

We can structure proofs to follow the
style of calculational or equational
reasoning popularized in classic texts <cit.>
and implemented in  <cit.>
and  <cit.>.

To this end, we have developed a library
of proof combinators that permits reasoning
about equalities and linear arithmetic.

“Equation” Combinators

We equip with a family of
equation combinators, "op", for
logical operators in the theory QF-UFLIA,
"op" $\in \{ =, \not =, \leq, <, \geq, > \}$.

In Haskell code, to avoid collisions with existing operators,
we further append a colon “":"” to these operators, so that “$=$”
becomes the Haskell operator "(=:)".

The refinement type of "op"  requires
that $x \odot y$ holds and then ensures
that the returned value is equal to "x".

For example, we define "(=:)" as:

(=:) :: x:a -> y: a | x = y  ->  v:a | v = x
x =: _ = x

and use it to write the following equational proof:

fib2_1 ::  !fib! 2 = 1
fib2_1 =  #fib# 2 =: #fib# 1 + #fib# 0 =: 1 ** QED

where "** QED" constructs proof terms by
casting expressions to in a post-fix

data $\tqed$ = QED            (**) :: a -> $\tqed$ -> $\typp$
_ ** QED = ()

Proof Arguments
Often, we need to compose lemmas into larger
theorems. For example, to prove "!fib! 3 = 2" we
may wish to reuse "fib2_1" as a lemma.

We do so by defining a variant of "(=:)", written as "(=?)",
that takes an explicit proof argument:

(=?) :: x:a -> y:a ->  $\typp$ | x = y  ->  v:a | v = x
x =? _ _ = x

We use the "(=?)" combinator to prove that "!fib! 3 = 2".

fib3_2 ::  !fib! 3 = 2
fib3_2 = (#fib# 3 =: fib 2 + #fib# 1 =? 2 dollar fib2_1) ** QED

Here "fib 2" is not important to unfold, because "fib2_1"
already provides the same information.

“Because” Combinators
Observe that the proof term "fib3_2" needs parentheses,
since Haskell's "(dollar)" operator has the lowest (0) precedence.

To omit parentheses in proof terms, we define
a “because” combinator that operates exactly like Haskell's
"(dollar)" operator, but has the same precedence as the proof combinators
"(=:)" and "(=?)".

($\because$) :: ($\typp$ -> a) -> $\typp$ -> a
f $\because$ y = f y

We use the “because” combinator to remove the parentheses from the proof term

fib3_2 ::  !fib! 3 = 2
fib3_2 = #fib# 3 =: fib 2 + #fib# 1 =? 2 $\because$ fib2_1 ** QED

Optional Proof Arguments

Finally, we unify both combinators "(=:)" and "(=?)"
using type classes to define the class method "(=.)"
that takes an optional proof argument, and
generalize such definitions for each operator in "op".

We define the class "OptEq" to have one method "(=.)"
that takes two arguments of type "a", to be compared
for equality, and returns a value of type "r".

class OptEq a r where
(=.) :: a -> a -> r

When instantiating the result type to be the same as the argument type "a",
"(=.)" behaves as "(=:)".

instance (a b) => OptEq a b where
(=.) :: x:a ->  y:a | x = y  ->  v:b | v = x

When the result type is instantiated to be
a function that given a proof term "$\typp$"
returns the argument type "a",
"(=.)" behaves exactly as "(=?)".

instance (a b) => OptEq a ($\typp$ -> b) where
(=.) :: x:a -> y:a ->  $\typp$ | x = y  ->  v:a | v = x

Thus, "(=.)" takes two arguments to be compared for equality
and, optionally, a proof term argument.

With this, the proof term "fib3_2" is simplified to

fib3_2 ::  !fib! 3 = 2
fib3_2 = #fib# 3 =. fib 2 + #fib# 1 =. 2 $\because$ fib2_1 ** QED

Arithmetic and Ordering

Next, lets see how we can use arithmetic and ordering to
prove that "fib" is (locally) increasing, for all $n$,
$\fib{n} \leq \fib{(n+1)}$.

type Up f = n:Nat ->  f n <= f (n + 1)

fibUp   :: Up fib
fibUp 0 =  #fib# 0 $<$. #fib# 1                          ** QED
fibUp 1 =  #fib# 1 <=. fib 1 + #fib# 0     =. #fib# 2     ** QED
fibUp n =  #fib# n <=. fib n + #fib# (n-1) =. #fib# (n+1) ** QED

Case Splitting

The proof "fibUp" works by splitting cases on the value of "n".

In the cases "0" and "1", we simply assert
the relevant inequalities. These are verified as the
reflected refinement unfolds the definition of
"fib" at those inputs.

The derived VCs are (automatically) proved
as the SMT solver concludes $0 < 1$ and $1 + 0 \leq 1$

When "n" is greater than one, "fib n" is unfolded
to  "fib (n-1) + fib (n-2)", which, as "fib (n-2)"
is non-negative, completes the proof.

Induction & Higher Order Reasoning

Refinement reflection smoothly accommodates induction
and higher-order reasoning.

For example, let's prove that every function "f"
that increases locally ("f z <= f (z+1)" for all "z")
also increases globally ("f x <= f y" for all "x < y")

type Mono = f:(Nat -> Integer) -> Up f -> x:Nat -> y: x < y  ->  f x <= f y

fMono :: Mono / [y]
fMono f up x y
| x+1 == y = f x <=. f (x+1) $\because$ up x <=. f y                          ** QED
| x+1  < y = f x <=. f (y-1) $\because$ fMono f up x (y-1) <=. f y $\because$ up (y-1) ** QED

We prove the theorem by induction
on "y" as specified by the
annotation "/ [y]" which states
that "y" is a well-founded
termination metric that decreases
at each recursive call <cit.>.

If "x+1 == y", then we call the "up x" proof argument.

Otherwise, "x+1 < y", and we use
the induction hypothesis apply
"fMono" at "y-1", after which
transitivity of the less-than
ordering finishes the proof.

We can apply the general
"fMono" theorem to prove that
"fib" increases monotonically:

fibMono :: n:Nat -> m: n < m  ->  !fib! n <= !fib! m
fibMono = fMono fib fibUp

§.§ Complete Verification: Automating Equational Reasoning

While equational proofs can be
very , writing them out
can quickly get exhausting.

Lets face it: "fib3_2" is doing
rather a lot of work just to
prove that "fib 3" equals "2"!

Happily, the calculational
nature of such proofs allows us
to develop the following proof
search algorithm that
is inspired by model checking <cit.>

* Guard Normal Form:

First, as shown in the definition
of "fibP" in  <ref>, each reflected
function is transformed into a
guard normal form

$\wedge_i (\pred_i \Rightarrow \fapp{\rfun}{x} = \body_i)$

a collection of guards $\pred_i$
and their corresponding definition $\body_i$.

* Unfolding:
Second, given a VC of the form
$\Penv \Rightarrow \pred$,
we iteratively unfold
function application terms in
$\Penv$ and $\pred$ by
instantiating them with
the definition corresponding to
an enabled guard, where
we check enabled-ness by
querying the SMT solver.

For example, given the VC
$\ttrue \Rightarrow \fib{3} = 2$,
the guard $3 > 1$ of the application $\fib{3}$ is
trivially enabled,
is true, hence we
strengthen the hypothesis
$\Penv$ with the equality
$\fib{3} = \fib{(3-1)} + \fib{(3-2)}$
corresponding to unfolding the
definition of "fib" at "3".

* Fixpoint:

We repeat the unfolding process
until either the VC is proved
or we have reached a fixpoint,
no further unfolding is

For example, the fixpoint
computation of $\fib{3}$ unfolds the definition
of "fib" at "3", "2", "1", and "0"
and then stops as no further
guards are enabled.

Automatic Equational Reasoning

In  <ref> we formalize
a notion of equational proof
and show that the proof search procedure
enjoys two key properties.

First, that it is guaranteed to find
an equational proof if one can be constructed
from unfoldings of function definitions.
(The user must still provide instantiations
of lemmas and induction hypotheses.)

Second, that under certain conditions readily
met in practice, it is guaranteed to terminate.

These two properties allow us to use to predictably automate proofs: the programmer needs
only to supply the relevant induction hypotheses
or helper lemma applications.

The remaining long chains of calculations
are performed automatically via SMT-based

That is, the user must provide case statements
and the recursive structure, but can elide
the long chains of =. applications.

To wit, with complete proof search,
the proofs of  <ref> shrink to:

fib3_2 :: !fib! 3 = 2       fMono :: Mono / [y]
fib3_2 = ()                 fMono f up x y
| x+1 == y = up x
| x+1  < y = up (y-1)           fMono up x (y-1)

where the combinator "p           q = ()"
inserts the propositions "p" and "q" to the
VC hypothesis.

vs. Axiomatization

Existing SMT based verifiers like
<cit.> and  <cit.>
use the classical axiomatic approach
to verify assertions over user-defined
functions like "fib".

In these systems, the function is encoded in the logic
as a universally quantified formula (or axiom):

$\forall n.\ \fibdef\ n$

after which the SMT solver may
instantiate the above axiom at
"3", "2", "1" and "0" in order to
automatically prove "fib 3 = 2".

The automation offered by axioms
is a bit of a devil's bargain,
as axioms render VC checking
undecidable, and in
practice automatic axiom
instantiation can easily
lead to infinite “matching loops”.

For example, the existence of
a term n in a VC can
trigger the above axiom,
which may then produce
the terms (n-1)
and (n-2), which
may then recursively
give rise to further
ad infinitum.

To prevent matching
loops an expert must
carefully craft “triggers”
or alternatively, provide
a “fuel” parameter
that bounds the depth of
instantiation <cit.>.

Both these approaches
ensure termination,
but can cause the
axiom to not be
instantiated at
the right places,
thereby rendering
the VC checking

The incompleteness
is illustrated by
the following example
from the benchmark
suite <cit.>

pos n | n < 0     = 0                test   :: y:y > 5 -> !pos! n = 3 + !pos! (n-3)
| otherwise = 1 + pos (n-1)    test _ = ()

(and 's) fuel-based approach fails
to check the above, when the fuel value is less
than $3$. One could simply raise-the-fuel-and-try-again
but at what point does the user know when to stop?

In contrast, (1) does not require any fuel
parameter, (2) is able to automatically perform
the required unfolding to verify this example,
and (3) is guaranteed to terminate.

app_assoc :: AppendAssoc
app_assoc [] ys zs
= ([] ++ ys) ++ zs
=. ys ++ zs
=. [] ++ (ys ++ zs)         ** QED
app_assoc (x:xs) ys zs
= ((x : xs) ++  ys)  ++ zs
=. (x : (xs ++  ys)) ++ zs
=.  x :((xs ++  ys)  ++ zs)
$\because$ app_assoc xs ys zs
=.  x : (xs ++ (ys   ++ zs))
=. (x : xs) ++ (ys   ++ zs) ** QED

app_assoc             :: AppendAssoc
app_assoc []     ys zs = ()
app_assoc (x:xs) ys zs = app_assoc xs ys zs

app_right_id          :: AppendNilId
app_right_id []        = ()
app_right_id (x:xs)    = app_right_id xs

map_fusion            :: MapFusion
map_fusion f g []      = ()
map_fusion f g (x:xs)  = map_fusion f g xs

(L) Equational proof of append associativity.   (R) proof, also of append-id and map-fusion.

§.§ Case Study: Laws for Lists

Reflection and are not limited to integers.  We end the
overview by showing how they verify textbook properties of lists
equipped with append ("++") and "map" functions:

reflect (++) :: [a] -> [a] -> [a]       reflect map :: (a -> b) -> [a] -> [b]
[]     ++ ys = ys                       map f []     = []
(x:xs) ++ ys = x : (xs ++ ys)           map f (x:xs) = f x : map f xs

In  <ref>
we will describe how the reflection mechanism
illustrated via "fibP" is extended to account for ADTs
using SMT-decidable selection and projection operations,
which reflect the definition of "xs ++ ys" into the refinement as:

$\ite{\mathtt{isNil}\ \mathit{xs}}
{\mathtt{sel1}\ \mathit{xs}\
\dcons\
(\mathtt{sel2}\ \mathit{xs} \ \mathtt{++}\  \mathit{ys})}$.

We require an explicit "reflect" annotation
as not all Haskell functions can be
reflected into logic, either because it
is unsound to do so (due to divergence)
or because of limitations of our current

Recall that verifies that all reflected functions,
like "(++)" and "map" here, are total <cit.>
and rejects the code otherwise.

We can specify various laws about lists with refinement types.
For example, the below laws state that

(1) appending to the right is an identity operation,

(2) appending is an associative operation, and

(3) map distributes over function composition:

type AppendNilId = xs:_ ->  xs ++ [] = xs
type AppendAssoc = xs:_ -> ys:_ -> zs:_ ->  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
type MapFusion   = f:_  -> g:_  -> xs:_ ->  map (f . g) xs = map f (map g xs)

On the right in Figure <ref>
we show the proofs of these laws using ,
which should be compared to the classical equational
proof  by <cit.>, shown on the left.

With , the user need only
provide the high-level structure
— the case splits and invocations
of the induction hypotheses —
after which automatically
completes the rest of the equational

Thus using SMT-based , "app_assoc"
shrinks down to its essence: an induction
over the list "xs".

The difference is even more stark with
"map_fusion" whose full equational proof
is omitted, as it is twice as long.

vs. Normalization

The proofs in Figure <ref>
may remind readers familiar with Type-Theory
based proof assistants (Coq or
Agda) of the notions of
type-level normalization and
rewriting that permit similar
proofs in those systems.

While our approach of is
inspired by the idea of type
level computation, it differs
from it in two significant ways.

First, from a theoretical point of view,
SMT logics are not equipped with any notion
of computation, normalization, canonicity
or rewriting.
Instead, our algorithm shows how
to emulate those ideas by asserting
equalities corresponding to function
definitions (Theorem <ref>).

Second, from a practical perspective,
the combination of (decidable) SMT-based
theory reasoning and 's proof search
can greatly simplify verification.

For example, consider the "swap" function
from <cit.>'s textbook:

swap :: [Integer] -> [Integer]
swap (x1:x2:xs) = if x1 > x2 then x2:x1:x2 else x1:x2:xs
swap xs         = xs

In Figure <ref> we show four proofs
that "swap" is idempotent:

Appel's proof using (simplified by
the use of a hint database and the
arithmetic tactic "omega"), its variant in
(for any Decidable Partial Order),
the proof, and
a proof using the verifier.

It is readily apparent that 's
proof search, working
hand-in-glove with SMT-based theory
reasoning, makes proving the result
trivial in comparison to or .

Of course, proof assistants like
, , and Isabelle
emit easily checkable certificates
and have decades-worth of tactics,
libraries, and proof scripts that
enable large scale proof engineering.

On the other hand, 's fuel-based
axiom instantiation automatically
unfolds the definition of "swap" twice,
thereby completing the proof
without any user input.

These heuristics are
orthogonal to  and can
be combined with it, if the user
wishes to trade off predictability
for even more automation.

Proofs that  is idempotent with
, , and .

We saw an overview of an SMT-automated refinement
type checker that achieves SMT-decidable checking
by restricting verification conditions to be
quantifier-free and hence, decidable.

In existing SMT-based verifiers () there
are two main reasons to introduce quantifiers, namely

(1) to express quantified specifications and
(2) to encode the semantics of user-defined functions.

Next, we use propositions-as-types to encode
quantified specifications and in  <ref>
we show how to encode the semantics of user-defined functions
via refinement reflection.

§ EMBEDDING NATURAL DEDUCTION WITH REFINEMENT TYPES

In this section we show how user-provided
quantified specifications
can be naturally encoded using
$\lambda$-abstractions and
dependent pairs to encode
universal and existential
quantification, respectively.
Proof terms can be generated
using the standard natural
deduction derivation rules,
following Propositions as Types <cit.>
(also known as the Curry-Howard
isomorphism <cit.>).

What is new is that we exploit this encoding to show for the first time that a refinement
type system can represent any proof
in Gentzen's natural deduction <cit.>
while still taking advantage of
SMT decision procedures to automate the
quantifier-free portion of natural
deduction proofs.

For simplicity, in this section we assume
all terms are total.

§.§ Propositions: Refinement Types

Figure <ref> maps logical predicates
to types constructed over quantifier-free refinements.

Native terms

Native terms consist of all of the
(quantifier-free) expressions
of the refinement languages.

In  <ref>
we formalize refinement typing
in a core calculus where
refinements include (quantifier-free)
terminating expressions.

Boolean connectives
Implication $\formula_1 \Rightarrow \formula_2$
is encoded as a function from the proof of
$\formula_1$ to the proof of $\formula_2$.

Negation is encoded as an implication where
the consequent is "False".

Conjunction $\formula_1 \land \formula_2$
is encoded as the pair "($\formula_1$, $\formula_2$)"
that contains the proofs of both conjuncts

and disjunction $\formula_1 \lor \formula_2$
is encoded as the sum type "Either"
that contains the proofs of one of
the disjuncts, where "data Either a b = Left a | Right b".

Universal quantification $\forall x. \formula$
is encoded as lambda abstraction $x:\typ \rightarrow \formula$
and eliminated by function application.

Existential quantification $\exists x. \formula$
is encoded as a dependent pair "(x::$\typ$, $\formula$)"
that contains the term $x$ and a proof of a formula
that depends on $x$.

Even though refinement type systems do not
traditionally come with explicit syntax for
dependent pairs, one can encode dependent
pairs in refinements using abstract
refinement types <cit.>
which do not add extra complexity
to the system.

Consequently, we add the syntax for
dependent pairs in Figure <ref>
as syntactic sugar for abstract refinements.

§.§ Proofs: Natural Deduction

We overload to be both a proposition and
a refinement type.

We connect these two meanings of by
using the Propositions as Types <cit.>,
to prove that if there exists an expression (or proof term) with
refinement type , then the proposition
is valid.

We construct proofs terms using Gentzen's
natural deduction system <cit.>,
whose rules map directly to refinement type

The rules for natural deduction arise from the propositions-as-types reading
of the standard refinement type
checking rule (to be defined in
<ref>) e
as “is provable under the assumptions of ”.

We write
for Gentzen's natural deduction judgment
“under assumption , proposition holds”.

Then, each of Gentzen's logical rules
can be recovered from the rules in
Figure <ref> by rewriting
each judgment e
of as .

For example, conjunction and universal
elimination can be derived as:

\inference{
\gentzenValid{\env}{{\formula_1} \lor{\formula_2}} &&
\gentzenValid{\env,\formula_1}{\formula} &&
\gentzenValid{\env,\formula_2}{\formula} &&
\gentzenValid{\env}{\formula}
\lor\small{\textsc{\!-E}}
\quad
\inference{
\gentzenValid{\env}{e_x\ \text{term}} &&
\gentzenValid{\env}{\forall x. \formula}
\gentzenValid{\env}{\formula\subst{x}{e_x}}
\forall\small{\textsc{\!-E}}

Programs as Proofs

As Figure <ref> directly maps
natural deduction rules to derivations
that are accepted by refinement typing,
we conclude that if there exists a
natural deduction derivation for a
proposition , then there
exists an expression that has the refinement type .

If ,
then we can construct an $e$ such that e.

Note that our embedding is not an isomorphism,
since the converse of Theorem <ref> does not hold.

As a counterexample, the law of the excluded middle
can be proved in our system
(we can construct an "Either" term $e$, so that
$\ch{\bind{p}{\proofterm{\typbool\ | \ \etrue}}}{e}{p\lor\neg p}$),
but cannot be proved using natural deduction
($\gentzenValid{{\proofterm{\etrue}}\not}{p\lor\neg p}$).

The reason for that is that our system is using the classical logic
of the SMTs, which includes the law of the excluded middle.
On the contrary, in intuitionistic systems that also encode natural deduction
(, , )
the law of the excluded middle should be axiomatized.

§.§ Examples

Next, we illustrate our encoding
with examples of proofs for
quantified propositions
ranging from

textbook logical tautologies,

properties of datatypes like lists,

and induction on natural numbers.

Natural Deduction as Type Derivation

We illustrate the mapping from natural deduction rules to typing rules
in Figure <ref> which uses typing judgments to express
Gentzen's proof of the proposition

\phi \equiv (\exists x. \forall y. (p\ x\ y)) \Rightarrow (\forall y. \exists x. (p\ x\ y))

Read bottom-up, the derivation provides a proof of .
Read top-down, it constructs a proof of the formula
as the term

$\lambda e\ y. \texttt{case}\ e\ \texttt{of}\ \{
(x,e_x) \rightarrow (x, e_x\ y)\}$.

This proof term corresponds directly to the following Haskell expression
that typechecks with type .

exAll :: p:(a -> a -> Bool) -> (x::a, y:a -> p x y) -> y:a -> (x::a, p x y)
exAll _ = y -> case e of (x, ex) -> (x, ex y)

\inference{
\inference{
\inference{
\bind{e}{\formulap},
\bind{y}{\typ_y}
\vdash
\formulap &&
\inference{
\bind{e}{\formulap},
\bind{y}{\typ_y},
\bind{x}{\type_x},
\bind{e_x}{\formulax}
\vdash
\formulax
\\
\bind{e}{\formulap},
\bind{y}{\typ_y},
\bind{x}{\type_x},
\bind{e_x}{\formulax}
\vdash
\typ_y
\bind{e}{\formulap},
\bind{y}{\typ_y},
\bind{x}{\type_x},
\bind{e_x}{\formulax}
\vdash
e_x\ y
p\ x\ y
\bind{e}{\formulap},
\bind{y}{\typ_y}
\vdash
\texttt{case}\ e\ \texttt{of}\ \{
(x,e_x) \rightarrow (x, e_x\ y)
\}
\exists x. (p\ x\ y)
\bind{e}{\formulap}
\vdash
\lambda y. \texttt{case}\ e\ \texttt{of}\ \{
(x,e_x) \rightarrow (x, e_x\ y)
\}
\forall y. \exists x. (p\ x\ y)
\emptyset
\vdash
\lambda e\ y. \texttt{case}\ e\ \texttt{of}\ \{
(x,e_x) \rightarrow (x, e_x\ y)
\}
{(\exists x. \forall y. (p\ x\ y)) \Rightarrow (\forall y. \exists x. (p\ x\ y))}
\impIntro

Proof of $(\exists x. \forall y. (p\ x\ y)) \Rightarrow (\forall y. \exists x. (p\ x\ y))$
$\formulap \equiv \exists x. \forall y. (p\ x\ y)
\formulax \equiv \forall y. (p\ x\ y)

SMT-aided proofs
The great benefit of using refinement types
to encode natural deduction is that the quantifier-free
portions of the proof can be automated via SMTs.

For every quantifier-free proposition ,
you can convert between $\{\formula\}$,
where is treated as an SMT-proposition
and , where is treated as a
type; and this conversion goes both ways.

For example, let $\formula \equiv p \land (q \lor r)$.

Then "flatten" converts from to
$\{\formula\}$ and "expand" the other way,
while this conversion is SMT-aided.

flatten :: p:_ -> q:_ -> r:_-> (p, Either q r) -> p        (q || r)
flatten (pf, Left  qf) = pf           qf
flatten (pf, Right rf) = pf           rf

expand :: p:_ -> q:_ -> r:_ -> p        (q || r) -> (p, Either q r)
expand proof | q = (proof, Left  proof)
expand proof | r = (proof, Right proof)

Distributing Quantifiers

Next, we construct the proof terms needed
to prove two logical properties:
that existentials distribute over disjunctions

and foralls over conjunctions,

\begin{align}
\formula_\exists \ & \equiv (\exists x. p\ x \lor q\ x) \Rightarrow ((\exists x. p\ x) \lor (\exists x. q\ x))
\label{eq:ex:or} \\
\formula_\forall \ & \equiv (\forall x. p\ x \land q\ x) \Rightarrow ((\forall x. p\ x) \land (\forall x. q\ x))
\label{eq:ex:and}
\end{align}

The specification of these properties requires
nesting quantifiers inside connectives and
vice versa.

The proof of $\formula_\exists$ (<ref>)
proceeds by existential case splitting and introduction:

exDistOr :: p:_ -> q:_ -> (x::a, Either p x q x)
-> Either (x::a, p x) (x::a, q x)
exDistOr _ _ (x, Left  px) = Left  (x, px)
exDistOr _ _ (x, Right qx) = Right (x, qx)

Dually, we prove $\formula_\forall$ (<ref>) via
a $\lambda$-abstraction and case spitting
inside the conjunction pair:

allDistAnd :: p:_ -> q:_ -> (x:a->(p x, q x))
-> ((x:a->p x), (x:a->q x))
allDistAnd _ _ andx = ( (-> case andx x of (px, _) -> px)
, (-> case andx x of (_, qx) -> qx) )

The above proof term exactly corresponds to its natural deduction proof derivation
but using SMT-aided verification can get simplified to the following

allDistAnd _ _ andx = (pf, pf)
where pf x = case andx x of (px, py) -> px           py

Properties of User Defined Datatypes

As can describe properties
of data types like lists, we can prove
properties of such types, that for
every list "xs", if there exists a list
"ys" such that "xs == ys ++ ys" ,then
"xs" has even length.

$$\formula \equiv \forall xs. ((\exists ys.\ xs = ys \ \texttt{++}\ ys) \Rightarrow (\exists n. \texttt{len}\ xs = n + n))$$

The proof ("evenLen") proceeds by existential elimination and introduction
and uses the "lenAppend" lemma, which in turn uses induction on the
input list and to automate equational reasoning.

evenLen :: xs:[a]->(ys::[a],xs = ys ++ ys)->(n::Int,len xs = n+n)
evenLen xs (ys,pf) = (len ys, lenAppend ys ys           pf)

lenAppend :: xs:_ -> ys:_ -> len (xs ++ ys) = len xs + len ys
lenAppend []     _  = ()
lenAppend (x:xs) ys = lenAppend xs ys

Induction on Natural Numbers

Finally, we specify and verify induction on natural numbers:

\formula_{ind} \equiv  (p\ 0 \land (\forall n. p\ (n-1) \Rightarrow p\ n) \Rightarrow \forall n. p\ n)

The proof proceeds by induction (case splitting).

In the base case, "n == 0", the proof calls the left conjunct, which contains a proof of the base case.

Otherwise, "0 < n", and the proof applies the induction hypothesis to the right conjunct instantiated at "n-1".

ind :: p:_ -> (p 0,(n:Nat -> p (n-1) -> p n)) -> n:Nat -> p n
ind p (p0, pn) 0 = p0
ind p (p0, pn) n = pn n (ind p (p0, pn) (n-1))

§.§ Consequences

To summarize, we use the propositions-as-types
principle to make two important contributions.

First, we show that natural deduction reasoning
can smoothly co-exist with SMT-based verification
to automate the decidable, quantifier-free portions
of the proof.

andRefine :: b1:Bool -> b2:Bool -> (b1, b2) -> b1        b2
andRefine _ _ (b1, b2) = ()

Using "andRefine" the user does not have to explicitly eliminate "PAnd".
For instance the "forallAndDistr" proof from  <ref>
simplifies to the following.

forallAndDistr _ _ andx = (fAndG, fAndG)
where fAndG = andRefine (f x) (g x) (andx x)

On the other direction, we reify SMT conjunction by using
$\formula_1 \land \formula_2$
as a proof for each conjunct $\formula_1$ and $\formula_2$
that can later be used in natural deduction derivations.

andReify :: b1:Bool -> b2:Bool -> b1        b2 -> (b1, b2)
andReify _ _ b = (b, b)

Second, we show for the first time how
natural deduction proofs can be encoded
in refinement type systems like and we expect this encoding to extend,
in a straightforward manner to other
SMT-based deductive verifiers
(and ).

This encoding shows that refinement type systems
are expressive enough to encode any intuitionistic natural deduction proof,
gives a guideline for encoding proofs
with nested quantifiers, and provides
a pleasant implementation of
natural deduction that

is pedagogically useful.

§ REFINEMENT REFLECTION:

Refinement reflection encodes recursive functions
in the quantifier-free, SMT logic and it is
formalized in three steps.

First, we develop a core calculus with an
undecidable type system based on denotational
semantics and prove it sound.

Next, in  <ref> we define
a language that soundly approximates while enabling decidable, SMT-based type checking.

Finally, in  <ref> we develop a complete
proof search algorithm to automate equational reasoning.

§.§ Syntax

Figure <ref> summarizes the syntax of ,
which is essentially the calculus  <cit.>
with explicit recursion and a special $\erefname$ binding
to denote terms that are reflected into the refinement logic.

The elements of are constants, values,
expressions, binders, and programs.

The constants of include primitive relations $\odot$,
here, the set $\{ =, <\}$.

Moreover, they include the
booleans $\etrue$, $\efalse$,
integers $\mathtt{-1}, \mathtt{0}$, $\mathtt{1}$, ,
and logical operators $\mathtt{\land}$, $\mathtt{\lnot}$, .

Data Constructors

Data constructors are special constants.

For example, the data type , which represents
finite lists of integers, has two data constructors: $\dnull$ (nil)
and $\dcons$ (cons).

Values & Expressions

The values of include
constants, $\lambda$-abstractions
$\efun{x}{\typ}{e}$, and fully
applied data constructors $D$
that wrap values.

The expressions of include values, variables $x$,
applications $\eapp{e}{e}$, and
$\mathtt{case}$ expressions.

Binders & Programs

A binder $\bd$ is a series of possibly recursive
$\mathtt{let}$ definitions, followed by an expression.

A program is a series of $\erefname$
definitions, each of which names a function
that is reflected into the refinement
logic, followed by a binder.

The stratification of programs via binders
is required so that arbitrary recursive definitions
are allowed in the program but cannot be inserted into the logic
via refinements or reflection.

(We can allow non-recursive $\mathtt{let}$
binders in expressions $e$, but omit them for simplicity.)

§.§ Operational Semantics

We define $\hookrightarrow$ to be the small step, call-by-name
$\beta$-reduction semantics for .

We evaluate reflected terms
as recursive $\mathtt{let}$ bindings, with termination
constraints imposed by the type system:

\erefb{x}{\gtyp}{e}{\prog}
\hookrightarrow
\eletb{x}{\gtyp}{e}{\prog}

We define $\evalsto{}{}$ to be the reflexive,
transitive closure of $\evals{}{}$.

Moreover, we define $\betaeq{}{}$ to be the reflexive,
symmetric, and transitive closure of $\evals{}{}$.

Constants Application of a constant requires the
argument be reduced to a value; in a single step, the
expression is reduced to the output of the primitive
constant operation, ${c\ v} \hookrightarrow \ceval{c}{v}$.

For example, consider $=$, the primitive equality
operator on integers.

We have $\ceval{=}{n} \defeq =_n$
where $\ceval{=_n}{m}$ equals iff $m$ is the same as $n$.

We assume that the equality operator
is defined for all values,
and, for functions, is defined as
extensional equality.

That is, for all
$f$ and $f'$,
$\evals{(f = f')}{\etrue}$
$\forall v.\ \betaeq{f\ v}{f'\ v}$.

We assume source terms only contain implementable equalities
over non-function types; while function extensional equality only
appears in refinements.
This statement is very unclear to me.

§.§ Types

types include basic types, which are refined with predicates,
and dependent function types.

Basic types comprise integers, booleans, and a family of data-types
$T$ (representing lists, trees ).

For example, the data type represents lists of integers.

We refine basic types with predicates (boolean-valued expressions ) to obtain
basic refinement types $\tref{v}{\btyp}{\refa}$.

We use to mark provably terminating
computations and use
refinements to ensure that if
then $e$ terminates.

As discussed by <cit.> termination labels
are checked using refinement types and are used
to ensure that refinements cannot diverge as required
for soundness of type checking under lazy evaluation.

Termination checking is crucial for this work,
as combined with checks for exhaustive definitions ( <ref>),
it ensures totality (well-formedness)
of expressions as required by
propositions-as-types ( <ref>)
and termination of ( <ref>).

Finally, we have dependent function types $\trfun{x}{\typ_x}{\typ}$
where the input $x$ has the type $\typ_x$ and the output $\typ$ may
refer to the input binder $x$.

We write $\btyp$ to abbreviate $\tref{v}{\btyp}{\etrue}$
and _x to abbreviate x_x, if
$x$ does not appear in $\typ$.

Kind of hard to read, even though $x$
isn't bound, the type still has $x$ as a
subscript. Compare to, $a:A \to B$, and
$A \to B$

Each type $\typ$ denotes a set of expressions $\interp{\typ}$,
that is defined via the operational semantics <cit.>.

Let $\shape{\typ}$ be the type we get if we erase all refinements
from $\typ$ and $\bhastype{}{e}{\shape{\typ}}$ be the
standard typing relation for the typed lambda calculus.

Then, we define the denotation of types as:

\begin{align*}
\interp{\tref{x}{\btyp}{r}} \defeq &\
\{ e \mid  \bhastype{}{e}{\btyp}
, \mbox{ if } \evalsto{e}{w} \mbox{ then } \evalsto{r\subst{x}{w}}{\etrue}
\}\\
\interp{\tref{x}{\btyp^\tlabel}{r}} \defeq &\
\interp{\tref{x}{\btyp}{r}} \cap \{ e \mid  \exists\ w. \evalsto{e}{w}\}\\
\interp{\trfun{x}{\typ_x}{\typ}} \defeq &\
\{ e \mid \bhastype{}{e}{\shape{\tfunbasic{\typ_x}{\typ}}}
, \forall e_x \in \interp{\typ_x}.\ (\eapp{e}{e_x}) \in \interp{\typ\subst{x}{e_x}}
\}
\end{align*}

For each constant $c$ we define its type c
such that $c \in \interp{\constty{c}}$.

For example,

\begin{array}{lcl}
\constty{3} &\doteq& \tref{v}{\tint^\tlabel}{v = 3}\\
\constty{+} &\doteq& \trfun{\ttx}{\tint^\tlabel}{\trfun{\tty}{\tint^\tlabel}{\tref{v}{\tint^\tlabel}{v = x + y}}}\\
\constty{\leq} &\doteq& \trfun{\ttx}{\tint^\tlabel}{\trfun{\tty}{\tint^\tlabel}{\tref{v}{\tbool^\tlabel}{v \Leftrightarrow x \leq y}}}\\
\end{array}

The right hand side is now a
refinement type, not a set like the
previous one.

§.§ Refinement Reflection

Reflection strengthens function output types
with a refinement that reflects the
definition of the function in the logic.

We do this by treating each

as a $\eletname$-binder

during type checking (rule $\rtreflect$ in Figure <ref>).

We write e for the reflection
of the term $e$ into the type $\typ$, defined as

\begin{array}{lcl}
\exacttype{\tref{v}{\btyp{^\tlabel}}{r}}{e}
& \defeq
& \tref{v}{\btyp{^\tlabel}}{r \land v = e}\\
\exacttype{\trfun{x}{\typ_x}{\typ}}{\efun{x}{}{e}}
& \defeq
& \trfun{x}{\typ_x}{\exacttype{\typ}{e}}
\end{array}

As an example, recall from  <ref>
that the "reflect fib" strengthens the type of
"fib" with the refinement "fibP".

That is, let the user specified type of be $t_\fibnameblack$ and the its definition be definition
$\lambda n . e_\fibnameblack$.

\begin{align*}
t_\fibnameblack & \defeq {\tfun{\ttnat}{\ttnat}} \\
e_\fibnameblack & \defeq \efib
\end{align*}

Then, the reflected type of will be:

\exacttype{t_\fibnameblack}{e_\fibnameblack} = \trfun{n}{\ttnat}{\tref{v}{\tint^\tlabel}{0 \leq v \land v = e_\fibname}}

Termination Checking
We defined ·· to be a partial
function that only reflects provably terminating expressions,
expressions whose result type is marked with .

If a non-provably terminating function is reflected
in an expression then type checking will
fail (with a reflection type error in the implementation).

This restriction is crucial for soundness,
as diverging expressions can lead to inconsistencies.

For example, reflecting the diverging "f x = 1 + f x"
into the logic leads to an inconsistent system that
is able to prove "0 = 1".

Automatic Reflection
Reflection of expressions into the refinements happens
automatically by the type system, not manually by the user.

The user simply annotates a function $f$ as $\annotReflect\ f$.

Then, the rule $\rtreflect$ in Figure <ref>
is used to type check the reflected function by strengthening
$f$'s result via ··.

Finally, the rule is used to check that the
automatically strengthened type of $f$ satisfies $f$'s implementation.

Hmm, the ordering is a bit weird here where there are a couple references to
fig 5, but then the next subsec starts with an introductory tone.

§.§ Typing Rules

Next, we present the type-checking rules of , as found in Figure <ref>.

Environments and Closing Substitutions
A type environment $\env$ is a sequence of type bindings
$\tbind{x_1}{\typ_1},\ldots,\tbind{x_n}{\typ_n}$. An environment
denotes a set of closing substitutions $\sto$ which are
sequences of expression bindings:
$\gbind{x_1}{e_1}, \ldots,$ $\gbind{x_n}{e_n}$ such that:

\interp{\env} \defeq  \{\sto \mid \forall \tbind{x}{\typ} \in \Env.
\sto(x) \in \interp{\applysub{\sto}{\typ}} \}

where $\applysub{\sto}{\typ}$ applies a substitution to a type (and
likewise $\applysub{\sto}{\prog}$, to a program).

A reflection environment $\RRenv$ is a sequence that binds the names
of the reflected functions with their definitions

A reflection environment respects a type environment
when all reflected functions satisfy their types:

\env \models \RRenv \defeq
\forall (\gbind{f}{e}) \in \RRenv.\;
\exists \typ.\;
(\tbind{f}{\typ}) \in \env \wedge

A judgment  states that
the program $\prog$ has the type $\typ$ in
the type environment $\env$ and the reflection environment $\RRenv$.
That is, when the free variables in $\prog$ are
bound to expressions described by $\env$, the
program $\prog$ will evaluate to a value
described by $\typ$.

All but two of the rules are standard <cit.>
except for the addition of the reflection environment $\RRenv$ at each rule.

First, rule is used to
extend the reflection environment with the binding of the function name
with its definition ($f \mapsto e$)
and moreover to strengthen the type of each
reflected binder with its definition, as described previously
in  <ref>.

Second, rule strengthens the expression with
a singleton type equating the value and the expression
(reflecting the expression in the type).

This is a generalization of the “selfification” rules
from <cit.> and is required to
equate the reflected functions with their definitions.

For example, the application "fib 1" is typed as
${\tref{v}{\tint^\tlabel}{\fibdef\ 1 \wedge v = \fib\ 1}}$ where
the first conjunct comes from the (reflection-strengthened)
output refinement of "fib" ( <ref>) and
the second comes from rule .

A judgment  states that
the refinement type $\typ$ is well-formed in
the environment $\env$.

Following <cit.>, $\typ$ is well-formed if all
the refinements in $\typ$ are $\tbool$-typed,
provably terminating expressions in $\env$.

A judgment _1_2 states
that the type $\typ_1$ is a subtype of
$\typ_2$ in the environments $\env$ and $\RRenv$.

Informally, $\typ_1$ is a subtype of $\typ_2$ if, when
the free variables of $\typ_1$ and $\typ_2$
are bound to expressions described by $\env$,
the denotation of $\typ_1$
is contained in the denotation of $\typ_2$.

Subtyping of basic types reduces to denotational
containment checking, shown in rule .

That is, $\typ_1$ is a subtype of $\typ_2$ under $\env$
if for any closing substitution $\sto$ in $\interp{\env}$,
$\interp{\applysub{\sto}{\typ_1}}$ is contained in

We prove that
typing implies denotational
inclusion and
evaluation preserves typing.

[Soundness of ]

* Denotations
If $\;\hastype{\env}{\RRenv}{\prog}{\typ}$, then
$\forall \sto\in \interp{\env}. \applysub{\sto}{\prog} \in \interp{\applysub{\sto}{\typ}}$.

* Preservation
If  ∅∅
and $\evalsto{\prog}{w}$, then $\hastype{\emptyset}{\emptyset}{w}{\typ}$.

The proofs can be found in <cit.>.
Theorem <ref> lets us
prove that if is a type
interpreted as a proposition
(using the mapping of Figure <ref>)
and if there exists a $\prog$ so that
the is valid.

For example, in  <ref> we verified
that the term proves
${\trfun{n}{\tnat}{\ttref{\fib{n} \leq \fib{(n+1)}}}}$.

Via soundness of , we get that for each valid input "n",
the result refinement is valid.

\forall n. \evalsto{0 \leq n}{\etrue} \Rightarrow \evalsto{\texttt{fib}\ n \leq \texttt{fib}\ {(n+1)}}{\etrue}

§ ALGORITHMIC CHECKING:

is a first order approximation of where higher-order features are
approximated with uninterpreted functions and the undecidable
type subsumption rule is replaced with a
decidable one (, ), yielding an sound
and decidable SMT-based algorithmic type system.

Figure <ref> summarizes the syntax
of , the sorted (SMT-)
decidable logic of quantifier-free equality,
uninterpreted functions and linear
arithmetic (QF-EUFLIA)  <cit.>.

The terms of include
integers $n$,
booleans $b$,
variables $x$,
data constructors $\dc$ (encoded as constants),
fully applied unary and binary operators,
and application $x\ \overline{\pred}$ of an uninterpreted function $x$.

The sorts of include the built-in
and to represent
integers and booleans and the
uninterpreted to represent data types.

The interpreted functions of , the logical constants $=$ and $<$,
have the function sort $\sort \rightarrow \sort$.

Other functional values in , reflected functions and
$\lambda$-expressions, are represented as
first-order values with
the uninterpreted sort .

§.§ Transforming into

The judgment
states that a $\corelan$ term $e$ is transformed,
under an environment $\env$, into a
$\smtlan$ term $\pred$.

If ${\tologicshort{\env}{\refa}{}{\pred}{}{}{}}$
and $\env$ is clear from the context we write
to denote the translation from to and back.

Most of the transformation rules are identity
and can be found in <cit.>.
Here we discuss the non-identity ones.

Embedding Types

We embed types into sorts as:

\begin{array}{lclclclclcl}
\tosmt{\tint}   & \defeq &  \tint  & \qquad\qquad &
\tosmt{T}       & \defeq &  \tuniv & \qquad\qquad &
\tosmt{\tref{v}{\btyp^{[\tlabel]}}{e}} &\defeq & \tosmt{\btyp} \\
\tosmt{\tbool}  & \defeq &  \tbool & \quad\quad &
&        &         & \quad\quad &
\tosmt{\trfun{x}{\typ_x}{\typ}} & \defeq & \tsmtfun{\tosmt{\typ_x}}{\tosmt{\typ}}
\end{array}$$

Embedding Constants

Elements shared on both and translate to themselves.

These elements include
and unary

SMT solvers do not support currying,
and so in , all function symbols
must be fully applied.

Thus, we assume that all applications
to primitive constants and data
constructors are fully applied, by converting
source terms like "(+ 1)" to
"(-> z + 1)".

Embedding Functions

As is first-order, we
embed $\lambda$s using the
uninterpreted function .

\inference{
\tologicshort{\env, \tbind{x}{\typ_x}}{e}{}{\pred}{}{}{} &
\hastype{\env}{\emptyset}{(\efun{x}{}{e})}{(\trfun{x}{\typ_x}{\typ})}\\
\tologicshort{\env}{\efun{x}{}{e}}{(\trfun{x}{\typ_x}{\typ})}
{\smtlamname{\tosmt{\typ_x}}{\tosmt{\typ}}\ {x}\ {\pred}}
{\sort'}{\smtenv, \tbind{f}{\sort'}}{\andaxioms{\{\axioms_{f_1}, \axioms_{f_2}\}}{\axioms}}
}%% [\lgfun]

The term $\efun{x}{}{e}$ of type
${\typ_x \rightarrow \typ}$ is transformed
${\smtlamname{\sort_x}{\sort}\ x\ \pred}$
of sort
${\tsmtfun{\sort_x}{\sort}}$, where

$\sort_x$ and $\sort$ are respectively
$\tosmt{\typ_x}$ and $\tosmt{\typ}$,

is a special uninterpreted function
of sort
${\sort_x \rightarrow \sort\rightarrow\tsmtfun{\sort_x}{\sort}}$,
$x$ of sort $\sort_x$ and $\pred$ of sort $\sort$ are
the embeddings of the binder and body, respectively.

As $\smtlamname{}{}$ is an SMT-function,
it does not create a binding for $x$.

Instead, $x$ is renamed to
a fresh SMT name.

Embedding Applications

We use defunctionalization <cit.> to
embed applications.

\inference{
\tologicshort{\env}{e_x}{\typ_x}{\pred_x}{\tosmt{\typ_x}}{\smtenv}{\axioms'}
\tologicshort{\env}{e}{\trfun{x}{\typ_x}{\typ}}{\pred}{\tsmtfun{\tosmt{\typ_x}}{\tosmt{\typ}}}{\smtenv}{\axioms}
\hastype{\env}{\emptyset}{e}{{\typ_x}\rightarrow{\typ}}
\tologicshort{\env}{e\ e_x}{\typ}{\smtappname{\tosmt{\typ_x}}{\tosmt{\typ}}\ {\pred}\ {\pred_x}}{\tosmt{\typ}}{\smtenv}{\andaxioms{\axioms}{\axioms'}}
}%% [\lgapp]

The term ${e\ e_x}$, where $e$ and $e_x$ have
types ${\typ_x \rightarrow \typ}$ and $\typ_x$,
is transformed to
${\tbind{\smtappname{\sort_x}{\sort}\ \pred\ \pred_x}{\sort}}$

$\sort$ and $\sort_x$ are $\tosmt{\typ}$ and $\tosmt{\typ_x}$,
is a special uninterpreted function of sort
${\tsmtfun{\sort_x}{\sort} \rightarrow \sort_x \rightarrow \sort}$,
$\pred$ and $\pred_x$ are the respective translations of $e$ and $e_x$.

Embedding Data Types

We embed data constructors to a predefined
constant ${\smtvar{\dc}}$ of
sort ${\tosmt{\constty{\dc}}}$:
\tologicshort{\env}{\dc}{\constty{\dc}}{\smtvar{\dc}}{\tosmt{\constty{\dc}}}{\emptyset}{\emptyaxioms}

For each datatype, we
create reflected functions
that check the top-level
constructor and select
their individual fields.

For example, for lists, we
create the functions

isNil []     = True         isCons (x:xs) = True          sel1 (x:xs) = x
isNil (x:xs) = False        isCons []     = False         sel2 (x:xs) = xs

The above selectors can be
modeled precisely in the refinement
logic via SMT support for ADTs <cit.>.

To generalize, let $\dc_i$ be a
data constructor such that
\constty{\dc_i} \defeq \typ_{i,1} \rightarrow \dots \rightarrow \typ_{i,n} \rightarrow \typ
Then check
${\checkdc{{\dc_i}}}$ has the sort
and select
${\selector{\dc}{i,j}}$ has the sort

Embedding Case Expressions

We translate case-expressions
of into nested $\mathtt{if}$
terms in , by using the check
functions in the guards and the
select functions for the binders
of each case.

\inference{
\tologicshort{\env}{e}{\typ_e}{\pred}{\tosmt{\typ_e}}{\smtenv}{\axioms} &&
\tologicshort{\env}{e_i\subst{\overline{y_i}}{\overline{\selector{\dc_i}{}\ x}}\subst{x}{e}}{\typ}{\pred_i}{\tosmt{\typ}}{\smtenv}{\axioms_i}
\tologicshort{\env}{\ecase{x}{e}{\dc_i}{\overline{y_i}}{e_i}}{\typ}
{\eif{\smtappname{}{}\ \checkdc{\dc_1}\ \pred}{\pred_1}{\ldots} \ \mathtt{else}\ \pred_n}{\tosmt{\typ}}{\smtenv}

The above translation yields the reflected definition
for append "(++)" from ( <ref>).

Semantic Preservation

The translation preserves the semantics of the expressions.

if ${\tologicshort{\env}{\refa}{}{\pred}{}{}{}}$,
then for every substitution $\theta$ and every logical model $\sigma$
that respects the environment $\env$
if $\evalsto{\applysub{\theta}{\refa}}{v}$
then $\sigma \models \pred = \tosmt{v}$.

What's a logical model?

§.§ Algorithmic Type Checking

We make the type checking from Figure <ref>
algorithmic by checking subtyping via our novel,
SMT-based Proof by Logical Evaluation().
Next, we formalize how makes checking algorithmic
and in  <ref> we describe the procedure in detail.

Verification Conditions

Recall that in   <ref> we defined
$\tosmt{\cdot}$ as the translation from to .

Informally, the implication or verification condition (VC)
$\tosmt{\env} \Rightarrow {\pred_1} \Rightarrow {\pred_2}$ is valid only if the
set of values described by $\pred_1$ is subsumed by
the set of values described by $\pred_2$ under the
assumptions of .

$\env$ is embedded into logic by conjoining
the refinements of terminating binders <cit.>:

\tosmt{\env} \defeq \bigcup_{x \in \env} \tosmt{\env, x} %\\
\quad \mbox{where we embed each binder as} \quad
\tosmt{\env, x} \defeq \begin{cases}
\tosmt{e}  & \text{if } \env(x)=\tref{x}{\btyp^{\tlabel}}{e}\\
\etrue & \text{otherwise}.
\end{cases}

Validity Checking
Instead of directly using the VCs to check validity of programs, we
use the procedure that strengthens the assumption environment
with equational properties.

given a

reflection environment $\RRenv$,

type environment $\env$, and

expression $e$,

the procedure $\pbe{\tosmt{\RRenv}}{\tosmt{\env}}{\tosmt{e}}$
— we will define $\tosmt{\RRenv}$ in  <ref> —
returns only when the expression $e$ evaluates
to under the reflection and type environments
and .

Subtyping via VC Validity Checking

We make subtyping, and hence, typing decidable,
by replacing the denotational base subtyping
rule with the conservative,
algorithmic version that uses
to check the validity of the

\inference{
\pbe{\tosmt{\RRenv}}{\tosmt{\env,\tbind{v}{\tref{v}{\btyp^\tlabel}{\refa_1}}}}{\tosmt{\refa_2}}
\pbeissubtype{\env}{\RRenv}{\tref{v}{\btyp}{\refa_1}}{\tref{v}{\btyp}{\refa_2}}

This typing rule is sound as functions reflected in always respect the typing environment (by construction)
and because is sound (Theorem <ref>).

If ve_1ve_2
then ve_1ve_2.

Soundness of

We write $\pbehastype{\env}{\RRenv}{e}{\typ}$
for the judgments that can be derived by the
algorithmic subtyping rule (instead of .)

Lemma <ref> implies the soundness of .

If e, then e.

§ COMPLETE VERIFICATION: PROOF BY LOGICAL EVALUATION

Next, we formalize our
Proof By Logical Evaluation
algorithm and show
that it is sound ( <ref>),
that it is complete with respect to
equational proofs ( <ref>),
and that it terminates ( <ref>).