# Proofs as stateful programs:
A first-order logic with abstract Hoare triples, and an interpretation into an
imperative language

Thomas Powell0000-0002-2541-4678  Department of Computer Science, University
of Bath<EMAIL_ADDRESS>
###### Abstract.

We introduce an extension of first-order logic that comes equipped with
additional predicates for reasoning about an abstract state. Sequents in the
logic comprise a main formula together with pre- and postconditions in the
style of Hoare logic, and the axioms and rules of the logic ensure that the
assertions about the state compose in the correct way. The main result of the
paper is a realizability interpretation of our logic that extracts programs
into a mixed functional/imperative language. All programs expressible in this
language act on the state in a sequential manner, and we make this intuition
precise by interpreting them in a semantic metatheory using the state monad.
Our basic framework is very general, and our intention is that it can be
instantiated and extended in a variety of different ways. We outline in detail
one such extension: A monadic version of Heyting arithmetic with a wellfounded
while rule, and conclude by outlining several other directions for future
work.

###### Key words and phrases:

Program extraction, modified realizability, imperative programs, state monad

##  1\. Introduction

The Curry-Howard correspondence lies at the heart of theoretical computer
science. Over the years, a multitude of different techniques for extracting
programs from proofs have been developed, the majority of which translate
formal proof systems into lambda calculi. As such, programs extracted from
proofs are typically conceived as pure functional programs.

Everyday programmers, on the other hand, often think and write in an
imperative paradigm, in terms of instructions that change some underlying
global state. This is reinforced by the fact that many of the most popular
programming languages, including C and Python, lean towards this style.
Imperative programs are nevertheless highly complex from a mathematical
perspective, and while systems such as Hoare logic [Hoa69] or separation logic
[Rey02] have been designed to reason about them, the formal extraction of
imperative programs from proofs has received comparatively little attention.

In this paper, we propose a new idea in this direction, developing a formal
system $\mathrm{SL}$ that enriches ordinary first-order logic with Hoare
triples for reasoning about an abstract global state. Sequents will have the
form $\Gamma\vdash\\{{\alpha}\cdot{A}\cdot{\beta}\\}$, where $A$ is a formula
and $\alpha,\beta$ assertions about the state, and proofs in the logic will
include both ordinary introduction and elimination rules for predicate logic,
together with special rules for reasoning about the state. We then construct a
stateful realizability interpretation (based on Kreisel’s modified
realizability [Kre59]) that relates formulas in $\mathrm{SL}$ to terms in a
mixed functional/imperative language $\mathrm{ST}$. Our main result is a
soundness theorem, which confirms that whenever a formula is provable in
$\mathrm{SL}$, we can extract a corresponding stateful realizing term in
$\mathrm{ST}$. While our initial soundness theorem focuses on pure predicate
logic, we subsequently show that it can be extended to arithmetic, where in
particular we are then able to extract programs that contain both recursion
and controlled while loops.

We are not the first to adapt traditional methods to extract imperative
programs: A major achievement in this direction, for example, is the monograph
[PCW05], which sets up a variant of intuitionistic Hoare logic alongside a
realizability translation into a standard imperative language. Other relevant
examples include [Atk09, CMM+09, DF89, Fil03, NAMB07, YHB07]. However, these
and almost all other prior work in this direction tend to focus on formal
verification, with an eye towards using proof interpretations as a method for
the synthesis of correct-by-construction software. In concrete terms, this
means that the formal systems tend to be quite detailed and oriented towards
program analysis, while the starting point is typically a program for which we
want to construct a verification proof, rather than a proof from which we hope
to extract a potentially unfamiliar program.

Our approach, on the other hand, is much more abstract, with an emphasis on
potential applications in logic and proof theory. Our basic system
$\mathrm{SL}$ makes almost no assumptions about the structure of the state and
what we are allowed to do with it. Rather, we focus on producing a general
framework for reasoning about ‘stateful formulas’, which can then be
instantiated with additional axioms to model concrete scenarios. The
simplicity and generality of our framework is its most important feature, and
we consider this work to be a first step towards a number of potentially
interesting applications. For this reason, we include not only an extension of
our system to a monadic theory of arithmetic, but conclude by sketching out
some additional ways in which we conjecture that our logic and interpretation
could be used and expanded, including the computational semantics of proofs
and probabilistic logic.

We take ideas from three main sources. The first is a case study of Berger et
al. [BSW14], in which a realizability interpretation is used to extract a
version of in-place quicksort, and where the imperative nature of the
extracted program is presented in a semantic way using the state monad. While
their program behaves imperatively “by-chance”, terms extracted from our logic
are forced to be imperative, and thus our framework offers one potential
solution to their open problem of designing a proof calculus which only yields
imperative programs. Indeed, an implementation of the insert sort algorithm is
formally extracted in Section 6 below. Our second source of inspiration is the
thesis of Birolo [Bir12], where a general monadic realizability interpretation
is defined and then used to give an alternative, semantic presentation of
learning-based interactive realizability [Asc11, Bd09]. However, our work goes
beyond this in that it also involves a monadic extension of the target logic,
whereas Birolo’s applies to standard first-order logic. Finally, a number of
ideas are taken from the author’s previous work [Pow18] on extracting stateful
programs using the Dialectica interpretation. While there the state is used in
a very specific and restricted way, here we use an analogous call-by-value
monadic translation on terms.

It is important to stress that we do not claim that our work represents an
optimal or complete method for extracting imperative programs from proofs, nor
do we claim that it is superior to alternative methods, including the
aforementioned works in the direction of verification, or, for instance,
techniques based on Krivine’s classical realizability [Kri09], which could be
viewed as imperative in nature. We simply offer what we consider to be a new
and interesting perspective that emphasises abstraction and simplicity, and
propose that our framework could prove valuable in a number of different
contexts.

#### Overview of the paper

The main technical work that follows involves the design of three different
systems, a realizability interpretation that connects them, and an
instantiation of this framework in the setting of first-order arithmetic,
namely:

  * •

A novel extension $\mathrm{SL}$ of predicate logic with abstract Hoare
triples, which can be extended with additional axioms for characterising the
state (Section 2).

  * •

A standard calculus $\mathrm{ST}$ for lambda terms with imperative commands,
which can again be extended with additional constants for interacting with the
state (Section 3).

  * •

A metalanguage $S^{\omega}$ into which both $\mathrm{SL}$ and $\mathrm{ST}$
can be embedded (Section 4), which is used to formulate the realizability
relation and prove its soundness (Section 5).

  * •

An instantiation of $\mathrm{SL}$ as a theory of arithmetic, with programs
extracted into an extension of $\mathrm{ST}$ with recursion and while loops
(Section 6).

Concrete examples are given, and potential applications surveyed in Section 7.

##  2\. The system $\mathrm{SL}$: First-order logic with state

We begin by introducing our target theory $\mathrm{SL}$ from which stateful
programs will be extracted. This is an extension of ordinary first-order logic
in the sense that the latter can always be embedded into $\mathrm{SL}$ (we
will make this precise in Proposition 1 below). Ultimately, we are interested
not so much in $\mathrm{SL}$ on its own, but in theories of the form
$\mathrm{SL}+\Delta_{H}+\Delta_{S}$, where $\Delta_{H}$ and $\Delta_{S}$ are
collections of (respectively non-computational and computational) axioms that
together characterise the state. Several concrete examples will be given to
illustrate this, and in Section 6 we present a variant of $\mathrm{SL}$ that
represents a theory of first-order arithmetic with state.

Before defining $\mathrm{SL}$, we give a standard presentation of first-order
intuitionistic predicate logic $\mathrm{PL}$, which serves as an opportunity
to fix our basic style of formal reasoning. The language of $\mathrm{PL}$
consists of the logical constants
$\wedge,\vee,\Rightarrow,\forall,\exists,\top,\bot$, variables $x,y,z,\ldots$,
along with function symbols $f,g,h,\ldots$ and predicate symbols
$P,Q,R,\ldots$, each with a fixed arity. We assume the existence of at least
one constant $c$. Terms are built from variables and function symbols as
usual, and formulas are built from prime formulas $P(t_{1},\ldots,t_{n})$,
$\top$ and $\bot$ using the logical constants. We use the usual abbreviation
$\neg A:\equiv A\Rightarrow\bot$. We work in a sequent style natural deduction
calculus, where sequents have the form $\Gamma\vdash_{I}A$ for some context
$\Gamma$ and formula $A$, and a context is a set of labelled assumptions of
the form $A_{1}^{u_{1}},\ldots,A_{n}^{u_{n}}$ for pairwise distinct labels
$u_{i}$. The axioms and rules of $\mathrm{PL}$ are as in Figure 1.

Figure 1. Axioms and rules of $\mathrm{PL}$
$\begin{gathered}\textbf{Propositional logic}\\\\[5.69054pt]
\Gamma\vdash_{I}A\ \ \ \mbox{if $A^{u}\in\Gamma$ for some
$u$}\qquad\Gamma\vdash_{I}\top\\\\[5.69054pt] {\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A\
\ \ \Gamma\vdash_{I}B$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to66.66669pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$\;\scriptstyle\wedge I$}}$}\hss}\kern
0.0pt}\kern 1.43518pt\hbox{\kern 10.96445pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}A\wedge B$}\kern 0.0pt$}}\kern 10.96445pt}}}\kern
15.51509pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A\wedge
B$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to44.73778pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\wedge E_{L}$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 9.5989pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}A$}\kern 0.0pt$}}\kern 9.5989pt}}}\kern
20.18176pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A\wedge
B$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to44.73778pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\wedge E_{R}$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 9.30551pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}B$}\kern 0.0pt$}}\kern 9.30551pt}}}\kern
20.52759pt}}}\\\\[5.69054pt] {\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
9.5989pt\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A$}}}\kern 9.5989pt}\kern
1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to44.73778pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\vee I_{L}$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma\vdash_{I}A\vee B$}\kern
0.0pt$}}}}}\kern 18.23732pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
9.30551pt\hbox{\hbox{\hbox{$\Gamma\vdash_{I}B$}}}\kern 9.30551pt}\kern
1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to44.73778pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\vee I_{R}$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma\vdash_{I}A\vee B$}\kern
0.0pt$}}}}}\kern 18.58315pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A\vee
B\ \ \ \Gamma,A^{u}\vdash_{I}C\ \ \ \Gamma,B^{v}\vdash_{I}C$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to149.36176pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\vee E$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 61.72966pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}C$}\kern 0.0pt$}}\kern 61.72966pt}}}\kern
17.45953pt}}}\\\\[5.69054pt] {\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
5.89703pt\hbox{\hbox{\hbox{$\Gamma,A^{u}\vdash_{I}B$}}}\kern 5.89703pt}\kern
1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to49.18219pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\Rightarrow I$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma\vdash_{I}A\Rightarrow
B$}\kern 0.0pt$}}}}}\kern 18.95952pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A\Rightarrow
B\ \ \ \Gamma\vdash_{I}A$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to89.72214pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$\;\scriptstyle\Rightarrow
E$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern 31.7977pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}B$}\kern 0.0pt$}}\kern 31.7977pt}}}\kern
20.90396pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}\bot$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to25.81773pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\bot E$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 0.13889pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}A$}\kern 0.0pt$}}\kern 0.13889pt}}}\kern
18.23732pt}}}\\\\[5.69054pt] \textbf{Quantifier rules}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A[y/x]$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to51.51674pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\forall I$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 6.51965pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}\forall xA$}\kern 0.0pt$}}\kern 6.51965pt}}}\kern
13.62624pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
5.69441pt\hbox{\hbox{\hbox{$\Gamma\vdash_{I}\forall xA$}}}\kern
5.69441pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to49.86626pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\forall E$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern 0.0pt\hbox{$\Gamma\vdash_{I}A[t/x]$}\kern
0.0pt$}}}}}\kern 15.57068pt}}}\\\\[5.69054pt] {\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}A[t/x]$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to49.86626pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\exists I$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 5.69441pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}\exists xA$}\kern 0.0pt$}}\kern 5.69441pt}}}\kern
13.62624pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{I}\exists
xA\ \ \ \Gamma,A[y/x]^{u}\vdash_{I}C$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to116.618pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$\;\scriptstyle\exists
E$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern 45.35779pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{I}C$}\kern 0.0pt$}}\kern 45.35779pt}}}\kern
15.57068pt}}}\\\\[5.69054pt] \mbox{for $\forall I$, $y\equiv x$ or $y$ not
free in $A$, and $y$ not free in $\Gamma$}\\\ \mbox{for $\exists E$, $y\equiv
x$ or $y$ not free in $A$, and $y$ not free in $C$ or
$\Gamma$.}\end{gathered}$

###  2.1. Stateful first-order logic

We now define our new logical system $\mathrm{SL}$, which is an extension of
ordinary first-order logic with new state propositions. To be more precise, we
extend the language of $\mathrm{PL}$ with a ternary operation
$\\{{-}\cdot{-}\cdot{-}\\}$, together with special state predicate symbols
$p,q,r,\ldots$, which also have a fixed arity. Terms of $\mathrm{SL}$ are the
same as those of $\mathrm{PL}$. On the other hand, there are two kinds of
formulas in $\mathrm{SL}$: state formulas and main formulas. A _state formula_
is defined using state predicate symbols and propositional connectives as
follows:

  * •

$\top$ and $\bot$ are state formulas,

  * •

if $p$ a state predicate symbol of arity $n$ and $t_{1},\ldots,t_{n}$ are
terms, then $p(t_{1},\ldots,t_{n})$ is a state formula,

  * •

if $\alpha,\beta$ are state formulas, so are $\alpha\wedge\beta$,
$\alpha\vee\beta$, $\alpha\Rightarrow\beta$.

A _main formula_ (or just _formula_) of $\mathrm{SL}$ is now defined as:

  * •

$\top$ and $\bot$ are formulas,

  * •

if $P$ is an ordinary predicate symbol of arity $n$ and $t_{1},\ldots,t_{n}$
are terms, then $P(t_{1},\ldots,t_{n})$ is a formula,

  * •

if $A,B$ are formulas, so are $A\wedge B$, $A\vee B$ and $\exists xA$,

  * •

if $A,B$ are formulas and $\alpha,\beta$ _state_ formulas, then
$A\Rightarrow\\{{\alpha}\cdot{B}\cdot{\beta}\\}$ and $\forall
x\,\\{{\alpha}\cdot{A}\cdot{\beta}\\}$ are formulas.

The notions of free and bound variables, along with substitution $\alpha[t/x]$
and $A[t/x]$ can be easily defined for both state and main formulas.

Analogous to the construction of formulas, our basic proof system uses the
auxiliary notion of a _state proof_ in order to define a main proof. A _state
sequent_ has the form $\Gamma\vdash_{H}\alpha$ where $\alpha$ is a state
formula and $\Gamma$ a set of labelled state formulas. A proof of
$\Gamma\vdash_{H}\alpha$ in $\mathrm{SL}$ is built from the axioms and rules
of _classical propositional logic_ i.e. the propositional axioms and rules as
set out in Figure 1 plus the law of excluded middle
$\Gamma\vdash_{H}\alpha\vee\neg\alpha$, together with a set $\Delta_{H}$ of as
yet unspecified state axioms of the form $\Gamma\vdash_{H}\alpha$.

A main sequent of $\mathrm{SL}$ has the form
$\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$, where $A$ is a formula
and $\alpha,\beta$ state formulas, and $\Gamma$ is a set of labelled main
formulas. A proof of $\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$ in
$\mathrm{SL}$ uses the axioms and rules given in Figure 2, together with a set
$\Delta_{S}$ of additional axioms.

Figure 2. Axioms and rules of $\mathrm{SL}$
$\begin{gathered}\textbf{Propositional axioms and rules}\\\\[5.69054pt]
\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\alpha}\\}\ \ \ \mbox{if
$A^{u}\in\Gamma$ for some
$u$}\qquad\Gamma\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\alpha}\\}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}\
\ \ \Gamma\vdash_{S}\\{{\beta}\cdot{B}\cdot{\gamma}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to122.37584pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\wedge_{S}I$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 24.82628pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A\wedge B}\cdot{\gamma}\\}$}\kern
0.0pt$}}\kern 24.82628pt}}}\kern 15.97624pt}}}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A\wedge
B}\cdot{\beta}\\}$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to73.20221pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\wedge_{S}E_{L}$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 9.5989pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$}\kern
0.0pt$}}\kern 9.5989pt}}}\kern 20.64291pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A\wedge
B}\cdot{\beta}\\}$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to73.20221pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\wedge_{S}E_{R}$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 9.30551pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{B}\cdot{\beta}\\}$}\kern
0.0pt$}}\kern 9.30551pt}}}\kern 20.98874pt}}}\\\\[5.69054pt]
{\vbox{\hbox{\kern 0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
9.5989pt\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$}}}\kern
9.5989pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to73.20221pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\vee_{S}I_{L}$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A\vee B}\cdot{\beta}\\}$}\kern
0.0pt$}}}}}\kern 18.69847pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
9.30551pt\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{B}\cdot{\beta}\\}$}}}\kern
9.30551pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to73.20221pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\vee_{S}I_{R}$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A\vee B}\cdot{\beta}\\}$}\kern
0.0pt$}}}}}\kern 19.0443pt}}}\\\\[5.69054pt] {\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A\vee
B}\cdot{\beta}\\}\ \ \
\Gamma,A^{u}\vdash_{S}\\{{\beta}\cdot{C}\cdot{\gamma}\\}\ \ \
\Gamma,B^{v}\vdash_{S}\\{{\beta}\cdot{C}\cdot{\gamma}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to232.31563pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\vee_{S}E$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 89.21385pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{C}\cdot{\gamma}\\}$}\kern
0.0pt$}}\kern 89.21385pt}}}\kern 17.92068pt}}}\\\\[5.69054pt]
{\vbox{\hbox{\kern 0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
21.90762pt\hbox{\hbox{\hbox{$\Gamma,A^{u}\vdash_{S}\\{{\alpha}\cdot{B}\cdot{\beta}\\}$}}}\kern
21.90762pt}\kern 1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to109.6678pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\Rightarrow_{S}I$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\gamma}\cdot{A\Rightarrow\\{{\alpha}\cdot{B}\cdot{\beta}\\}}\cdot{\gamma}\\}$}\kern
0.0pt$}}}}}\kern 18.86513pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A\Rightarrow\\{{\gamma}\cdot{B}\cdot{\delta}\\}}\cdot{\beta}\\}\
\ \ \Gamma\vdash_{S}\\{{\beta}\cdot{A}\cdot{\gamma}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to176.7196pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\Rightarrow_{S}E$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 61.67012pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{B}\cdot{\delta}\\}$}\kern
0.0pt$}}\kern 61.67012pt}}}\kern 20.80957pt}}}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{\bot}\cdot{\beta}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to54.28217pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\bot_{S}E$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 0.37836pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\gamma}\\}$}\kern
0.0pt$}}\kern 0.37836pt}}}\kern 18.69847pt}}}\ \ \ \mbox{for $\gamma$
arbitrary}\\\\[5.69054pt] \textbf{Quantifier rules}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha[y/x]}\cdot{A[y/x]}\cdot{\beta[y/x]}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to131.93475pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\forall_{S}I$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 14.26369pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\gamma}\cdot{\forall
x\,\\{{\alpha}\cdot{A}\cdot{\beta}\\}}\cdot{\gamma}\\}$}\kern 0.0pt$}}\kern
14.26369pt}}}\kern 14.64293pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{\forall
x\,\\{{\beta}\cdot{A}\cdot{\gamma}\\}}\cdot{\beta[t/x]}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to128.21262pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\forall_{S}E$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 13.01727pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A[t/x]}\cdot{\gamma[t/x]}\\}$}\kern
0.0pt$}}\kern 13.01727pt}}}\kern 16.58737pt}}}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A[t/x]}\cdot{\beta}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to78.33069pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\exists_{S}I$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 5.69441pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{\exists xA}\cdot{\beta}\\}$}\kern
0.0pt$}}\kern 5.69441pt}}}\kern 14.64293pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{\exists
xA}\cdot{\beta}\\}\ \ \
\Gamma,A[y/x]^{u}\vdash_{S}\\{{\beta}\cdot{C}\cdot{\gamma}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to172.32715pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle\exists_{S}E$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 59.21962pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{C}\cdot{\gamma}\\}$}\kern
0.0pt$}}\kern 59.21962pt}}}\kern 16.58737pt}}}\\\\[5.69054pt] \mbox{for
$\forall_{S}I$, $y\equiv x$ or $y$ not free in $A$, $\alpha$, $\beta$, and $y$
not free in $\Gamma$}\\\ \mbox{for $\exists_{S}E$, $y\equiv x$ or $y$ not free
in $A$, and $y$ not free in $C$, $\alpha$, $\beta$, $\gamma$ or
$\Gamma$.}\\\\[5.69054pt] \textbf{Basic Hoare rules}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\alpha\vdash_{H}\beta\
\ \ \Gamma\vdash_{S}\\{{\beta}\cdot{A}\cdot{\gamma}\\}\ \ \
\gamma\vdash_{H}\delta$}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to132.4573pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$\;\scriptstyle cons$}}$}\hss}\kern
0.0pt}\kern 1.43518pt\hbox{\kern 39.83237pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\delta}\\}$}\kern
0.0pt$}}\kern 39.83237pt}}}\kern 16.68294pt}}}\\\\[5.69054pt]
{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\vdash_{H}\alpha\vee\beta\
\ \ \Gamma\vdash_{S}\\{{\alpha\wedge\gamma}\cdot{A}\cdot{\delta}\\}\ \ \
\Gamma\vdash_{S}\\{{\beta\wedge\gamma}\cdot{A}\cdot{\delta}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to201.80643pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle cond$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 75.11678pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\gamma}\cdot{A}\cdot{\delta}\\}$}\kern
0.0pt$}}\kern 75.11678pt}}}\kern 17.04509pt}}}\\\\[5.69054pt]
\textbf{Additional axioms}\\\\[5.69054pt] \mbox{state axioms $\Delta_{H}$ of
the form $\Gamma\vdash_{H}\alpha$}\\\ \mbox{main axioms $\Delta_{S}$ of the
form $\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$}\end{gathered}$

We now make precise what we mean when we characterise $\mathrm{SL}$ as an
extension of standard first-order logic. The following is provable with an
easy induction over derivations in $\mathrm{PL}$:

######  Proposition 1.

For any formula $A$ of $\mathrm{PL}$ and state formula $\alpha$, define the
main formula $A_{\alpha}$ of $\mathrm{SL}$ by

  * •

$Q_{\alpha}:=Q$ for $Q$ atomic,

  * •

$(A\wedge B)_{\alpha}:=A_{\alpha}\wedge B_{\alpha}$, $(A\vee
B)_{\alpha}:=A_{\alpha}\vee B_{\alpha}$ and $(\exists x\,A)_{\alpha}:=\exists
x\,A_{\alpha}$,

  * •

$(A\Rightarrow
B)_{\alpha}:=A_{\alpha}\Rightarrow\\{{\alpha}\cdot{B_{\alpha}}\cdot{\alpha}\\}$
and $(\forall x\,A)_{\alpha}:=\forall
x\,\\{{\alpha}\cdot{A_{\alpha}}\cdot{\alpha}\\}$.

Then whenever $\Gamma\vdash_{I}A$ is provable in $\mathrm{PL}$, we have that
$\Gamma_{\alpha},\Delta\vdash_{S}\\{{\alpha}\cdot{A_{\alpha}}\cdot{\alpha}\\}$
is provable in $\mathrm{SL}$, where $\Delta$ is arbitrary and
$\Gamma_{\alpha}:=(A_{1})^{u_{1}}_{\alpha},\ldots,(A_{n})^{u_{n}}_{\alpha}$
for $\Gamma:=A_{1}^{u_{1}},\ldots,A_{n}^{u_{n}}$.

###  2.2. The intuition behind $\mathrm{SL}$

The intended semantic meaning of $\Gamma\vdash_{H}\alpha$ is that $\alpha$ can
be inferred from the assumptions $\Gamma$ for any fixed state. More
specifically, if we imagine a semantic variant $[\alpha](\pi)$ of each state
formula where now the dependency on an underlying state $\pi$ is made
explicit, the semantics of $\Gamma\vdash_{H}\alpha$ is just

$[\Gamma](\pi)\Rightarrow[\alpha](\pi)$

On the other hand, the intended meaning of
$\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$ is that from assumptions
$\Gamma$, if $\alpha$ holds with respect to some initial state, then we can
infer that $A$ is true and $\beta$ holds with respect to some modified state,
or more precisely:

$[\Gamma]\Rightarrow(\exists\pi\,[\alpha](\pi)\Rightarrow([A]\wedge\exists\pi^{\prime}\,[\beta](\pi^{\prime})))$
(1)

In particular, the computational interpretation of (1) above will be a program
that takes some input state $\pi$ satisfying $[\alpha](\pi)$ and returns a
realizer-state pair $\langle{x,\pi^{\prime}}\rangle$ such that $x$ realizes
$A$ and $[\beta](\pi^{\prime})$ holds.

Our semantic interpretation $[\cdot]$ will be properly defined in Section 4.
Crucially, in $\mathrm{SL}$ the state is _implicit_ , and so there are no
variables or terms of state type. The state will rather be made explicit in
our metatheory $S^{\omega}$. The main axioms and rules of $\mathrm{SL}$ simply
describe how this semantic interpretation propagates in a call-by-value manner
through the usual axioms and rules of first-order logic. The state itself is
brought into play through the Hoare rules along with the additional axioms
$\Delta_{H}$ and $\Delta_{S}$.

To give a more detailed explanation, consider the introduction rule
$\wedge_{S}I$. Semantically, the idea is that if

$\exists\pi\,[\alpha](\pi)\Rightarrow([A]\wedge\exists\pi_{1}\,[\beta](\pi_{1}))\
\ \ \mbox{and}\ \ \
\exists\pi_{1}\,[\beta](\pi_{1})\Rightarrow([B]\wedge\exists\pi_{2}\,[\gamma](\pi_{2}))$

both hold, then we can infer

$\exists\pi\,[\alpha](\pi)\Rightarrow([A]\wedge[B]\wedge\exists\pi_{2}\,[\gamma](\pi_{2}))$

and this can be regarded as a ‘stateful’ version of the usual conjunction
introduction rule. In particular, we note that this is no longer symmetric:
Informally speaking, $[A]$ is ‘proven first’, followed by $[B]$. Under our
realizability interpretation, this rule will correspond to realizer for
$\\{{\alpha}\cdot{A}\cdot{\beta}\\}$ being sequentially composed with a
realizer for $\\{{\beta}\cdot{B}\cdot{\gamma}\\}$.

Similarly, for the stateful quantifier rule $\forall_{S}I$, the premise
$\\{{\alpha[y/x]}\cdot{A[y/x]}\cdot{\beta[y/x]}\\}$ corresponds semantically
to

$\exists\pi\,[\alpha[y/x]](\pi)\Rightarrow[A[y/x]]\wedge\exists\pi^{\prime}\,[\beta[y/x]](\pi^{\prime})$

and so by the standard quantifier rule of ordinary predicate logic we would
have

$\forall
x(\exists\pi\,[\alpha](\pi)\Rightarrow[A]\wedge\exists\pi^{\prime}\,[\beta](\pi^{\prime}))$

From this we can directly infer

$\exists\pi\,[\gamma](\pi)\Rightarrow\forall
x(\exists\pi\,[\alpha](\pi)\Rightarrow[A]\wedge\exists\pi^{\prime}\,[\beta](\pi^{\prime}))\wedge\exists\pi\,[\gamma](\pi)$

for arbitrary $\gamma$, and the above now this has the right form, namely the
semantic interpretation of $\\{{\gamma}\cdot{\forall
x\,\\{{\alpha}\cdot{A}\cdot{\beta}\\}}\cdot{\gamma}\\}$.

We note that the traditional rules of Hoare logic correspond to certain simple
cases of our rules. For example, the composition rule could be viewed as
special case of $\wedge_{S}I$ for $A=B=\top$, more specifically the
derivation:

$\Gamma\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\beta}\\}$$\Gamma\vdash_{S}\\{{\beta}\cdot{\top}\cdot{\gamma}\\}$
$\;\scriptstyle\wedge_{S}I$
$\Gamma\vdash_{S}\\{{\alpha}\cdot{\top\wedge\top}\cdot{\gamma}\\}$
$\;\scriptstyle\wedge_{S}E_{L}$
$\Gamma\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\gamma}\\}$

In a similar spirit, the two Hoare rules of $\mathrm{SL}$ correspond to the
_consequence_ and _conditional_ rules of ordinary Hoare logic, with the
traditional conditional rule falling out as a special case of ours since we
assume $\Gamma\vdash_{H}\alpha\vee\neg\alpha$. In Section 6 we extend this
further by adding a controlled while loop to our logic. But for now, we
illustrate our logic with some very straightforward scenarios.

[Simple query and return] Consider a very simple state, on which we can
perform the following actions:

  1. (1)

Store any value from our domain of discourse in some query location.

  2. (2)

For the current value $x$ in the query location, return a suitable answer $y$
such that $P(x,y)$ holds for some fixed binary predicate system of the logic,
and store this value.

  3. (3)

Retrieve the computed value $y$ from the state.

We formalise those three actions by including two unary state predicates
$\mathsf{query}$ and $\mathsf{return}_{P}$, where $\mathsf{query}(x)$ denotes
that $x$ is currently stored in the query location, and
$\mathsf{return}_{P}(x)$ denotes that some $y$ satisfying $P(x,y)$ has been
returned. We would then add the following axioms to $\Delta_{S}$, which
intuitively represent each of the above actions:

  1. (1)

$\Gamma\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\mathsf{query}(x)}\\}$ where
$\alpha$ ranges over all state formulas,

  2. (2)

$\Gamma\vdash_{S}\\{{\mathsf{query}(x)}\cdot{\top}\cdot{\mathsf{return}_{P}(x)}\\}$

  3. (3)

$\Gamma\vdash_{S}\\{{\mathsf{return}_{P}(x)}\cdot{\exists
y\,P(x,y)}\cdot{\top}\\}$

The second rule should be regarded as representing an abstract updating of the
state where the return value is stored somewhere, and the third the act of
retrieval, where following the update we can now formally prove $\exists
y\,P(x,y)$. Note that the computational aspects of this interpretation will
only become apparent under the realizability interpretation, where a realizer
for $\\{{\mathsf{return}_{P}(x)}\cdot{\exists y\,P(x,y)}\cdot{\top}\\}$ will
be a function that accesses any state satisfying $\mathsf{return}_{P}(x)$ and
produces as output the $y$ satisfying $P(x,y)$ (See Example 5.2).

We can now, for example, derive the following theorem in
$\mathrm{SL}+\Delta_{H}+\Delta_{S}$ (for $\Delta_{H}=\emptyset$), where
$\alpha,\beta$ are any state formulas:

$\vdash_{S}\\{{\beta}\cdot{\forall x\,\\{{\alpha}\cdot{\exists
y\,P(x,y)}\cdot{\top}\\}}\cdot{\beta}\\}$

The derivation below is essentially a proof of $\forall x\exists y\,P(x,y)$
that, necessarily, utilising properties of the state:

$\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\mathsf{query}(x)}\\}$$\vdash_{S}\\{{\mathsf{query}(x)}\cdot{\top}\cdot{\mathsf{return}_{P}(x)}\\}$
$\;\scriptstyle\wedge_{S}I$
$\vdash_{S}\\{{\alpha}\cdot{\top\wedge\top}\cdot{\mathsf{return}_{P}(x)}\\}$
$\;\scriptstyle\wedge_{S}E_{L}$
$\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\mathsf{return}_{P}(x)}\\}$
$\vdash_{S}\\{{\mathsf{return}_{P}(x)}\cdot{\exists y\,P(x,y)}\cdot{\top}\\}$
$\;\scriptstyle\wedge_{S}I$ $\vdash_{S}\\{{\alpha}\cdot{\top\wedge\exists
y\,P(x,y)}\cdot{\top}\\}$ $\;\scriptstyle\wedge_{S}E_{L}$
$\vdash_{S}\\{{\alpha}\cdot{\exists y\,P(x,y)}\cdot{\top}\\}$
$\;\scriptstyle\forall_{S}I$ $\vdash_{S}\\{{\beta}\cdot{\forall
x\,\\{{\alpha}\cdot{\exists y\,P(x,y)}\cdot{\top}\\}}\cdot{\beta}\\}$

We note that while state formulas and actions are used in the _proof_ , if we
set $\alpha=\beta=\top$ then the components of the _theorem_ itself are just
formulas in ordinary first-order logic. A program corresponding to this
derivation will be formally extracted in Example 5.2, but referring to the
semantic explanations above, we can view each instance of $\wedge_{S}I$ in the
proof as a sequential composition of state actions (with $\wedge_{S}E$ just
cleaning up the central logical formula), and finally $\forall_{S}I$ is just
the stateful version of the usual $\forall$-introduction rule.

[Fixed-length array sorting] Let us now consider our state as an array of
length three, and elements in that array as having some order structure. We
formalise this in $\mathrm{SL}$ by introducing $1,2,3$ as constants
representing our three locations, along with two state predicates: a binary
predicate $\leq$ for comparing elements at locations $l$ and $l^{\prime}$, and
a nullary predicate $\mathsf{sorted}$ that declares that the state is sorted.
These can be characterised by adding the following axiom schemes, but to
$\Delta_{H}$ rather than $\Delta_{S}$ as they do not represent state _actions_
:

$\displaystyle\Gamma\vdash_{H}1\leq 2\wedge 2\leq 3\Rightarrow\mathsf{sorted}$
$\displaystyle\Gamma\vdash_{H}l\leq l^{\prime}\vee l^{\prime}\leq l\ \ \
\mbox{where $l,l^{\prime}$ range over $\\{1,2,3\\}$}$

We then allow a single action on our array, namely the swapping of a pair of
elements in the list. Suppose that $\alpha$ is a state formula of the form

$\alpha:\equiv l_{1}\leq l^{\prime}_{1}\wedge\ldots\wedge l_{n}\leq
l^{\prime}_{n}$ (2)

where $l_{i},l_{i}$ range over locations $\\{1,2,3\\}$. Now for
$l,l^{\prime}\in\\{1,2,3\\}$ let $\alpha[l\leftrightarrow l^{\prime}]$ denote
$\alpha$ where all instances of $l$ and $l^{\prime}$ are swapped, so that if
e.g. $\alpha=3\leq 2\wedge 1\leq 2\wedge 1\leq 3$ then

$\alpha[2\leftrightarrow 3]=2\leq 3\wedge 1\leq 3\wedge 1\leq 2$

We axiomatise the swapping of the values in locations of some arbitrary pair
$l,l^{\prime}\in\\{1,2,3\\}$ by adding to $\Delta_{S}$ all instances of

$\Gamma\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\alpha[l\leftrightarrow
l^{\prime}]}\\}$

where $\alpha$ ranges over state formulas of the form (2). The statement that
all arrays of length three can be sorted is then formulated as

$\vdash_{S}\\{{\top}\cdot{\top}\cdot{\mathsf{sorted}}\\}$

Let us now give a proof of this statement in
$\mathrm{SL}+\Delta_{H}+\Delta_{S}$. As with the previous example, we
emphasise that the underlying computation represented by this proof will only
become visible through the realizability interpretation.

First, let $\alpha:=1\leq 2\wedge 1\leq 3$, and define $\mathcal{D}_{1}$ as

$\vdash_{S}\\{{2\leq 3\wedge\alpha}\cdot{\top}\cdot{2\leq 3\wedge\alpha}\\}$
$\;\scriptstyle cons$ $\vdash_{S}\\{{2\leq
3\wedge\alpha}\cdot{\top}\cdot{\mathsf{sorted}}\\}$ $\vdash_{S}\\{{2\leq
3\wedge\alpha}\cdot{\top}\cdot{2\leq 3\wedge\alpha}\\}$ $\;\scriptstyle cons$
$\vdash_{S}\\{{2\leq 3\wedge\alpha}\cdot{\top}\cdot{\mathsf{sorted}}\\}$
$\;\scriptstyle 2\leftrightarrow 3$ $\vdash_{S}\\{{3\leq
2\wedge\alpha}\cdot{\top}\cdot{2\leq 3\wedge 1\leq 3\wedge 1\leq 2}\\}$
$\;\scriptstyle cons$ $\vdash_{S}\\{{3\leq
2\wedge\alpha}\cdot{\top}\cdot{\mathsf{sorted}}\\}$ $\;\scriptstyle cond[2\leq
3\vee 3\leq 2]$ $\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\mathsf{sorted}}\\}$

where for the left instance of $cons$ we use $2\leq
3\wedge\alpha\vdash_{H}\mathsf{sorted}$, in the right that $2\leq 3\wedge
1\leq 3\wedge 1\leq 2\vdash_{H}\mathsf{sorted}$, and for the final instance of
$cond$ we use $\vdash_{H}2\leq 3\vee 3\leq 2$. Now let $\mathcal{D}_{2}$ be
defined by

$\;\scriptstyle 1\leftrightarrow 2$ $\vdash_{S}\\{{2\leq 1\wedge 2\leq
3}\cdot{\top}\cdot{1\leq 2\wedge 1\leq 3}\\}$ $\mathcal{D}_{1}$
$\vdash_{S}\\{{1\leq 2\wedge 1\leq 3}\cdot{\top}\cdot{\mathsf{sorted}}\\}$
$\;\scriptstyle\wedge_{S}I$ $\vdash_{S}\\{{2\leq 1\wedge 2\leq
3}\cdot{\top\wedge\top}\cdot{\mathsf{sorted}}\\}$
$\;\scriptstyle\wedge_{S}E_{L}$ $\vdash_{S}\\{{2\leq 1\wedge 2\leq
3}\cdot{\top}\cdot{\mathsf{sorted}}\\}$

Then we have $\mathcal{D}_{3}$:

$\mathcal{D}_{2}$ $\vdash_{S}\\{{2\leq 1\wedge 2\leq
3}\cdot{\top}\cdot{\mathsf{sorted}}\\}$ $\\{{1\leq 2\wedge 2\leq
3}\cdot{\top}\cdot{1\leq 2\wedge 2\leq 3}\\}$ $\;\scriptstyle cons$
$\vdash_{S}\\{{1\leq 2\wedge 2\leq 3}\cdot{\top}\cdot{\mathsf{sorted}}\\}$
$\;\scriptstyle cond[2\leq 1\vee 1\leq 2]$ $\vdash_{S}\\{{2\leq
3}\cdot{\top}\cdot{\mathsf{sorted}}\\}$

where here $cond$ uses $\vdash_{H}2\leq 1\vee 1\leq 2$, and finally

$\vdash_{S}\\{{2\leq 3}\cdot{\top}\cdot{2\leq 3}\\}$ $\;\scriptstyle
2\leftrightarrow 3$ $\vdash_{S}\\{{3\leq 2}\cdot{\top}\cdot{2\leq 3}\\}$
$\;\scriptstyle cond[2\leq 3\vee 3\leq 2]$
$\vdash_{S}\\{{\top}\cdot{\top}\cdot{2\leq 3}\\}$ $\mathcal{D}_{3}$
$\vdash_{S}\\{{2\leq 3}\cdot{\top}\cdot{\mathsf{sorted}}\\}$
$\;\scriptstyle\wedge_{S}I$
$\vdash_{S}\\{{\top}\cdot{\top\wedge\top}\cdot{\mathsf{sorted}}\\}$
$\;\scriptstyle\wedge_{S}E_{L}$
$\vdash_{S}\\{{\top}\cdot{\top}\cdot{\mathsf{sorted}}\\}$

In contrast to Example 2.2 above, this is an example of a purely imperative
proof that involves no propositional formulas other than $\top$. As we will
see in Example 5.2, the proof corresponds to a purely imperative program.

##  3\. The system $\mathrm{ST}$: A simple functional/imperative term calculus

We now define our calculus $\mathrm{ST}+\Lambda_{S}$ whose terms will
represent realizers for proofs in $\mathrm{SL}+\Delta_{H}+\Delta_{S}$. This is
a standard typed lambda calculus for mixed functional and imperative programs,
and is defined to include basic terms together with additional constants in
some set $\Lambda_{S}$, where the latter are intuitively there to realize the
axioms in $\Delta_{S}$. Semantics for the terms will be given via a monadic
translation into the metalanguage defined in the next section. Types are
defined by the grammar

$X::=D\,|\,C\,|\,X\times X\,|\,X+X\,|\,X\to X$

while basic terms are defined as

$\displaystyle e::=$
$\displaystyle\mathsf{skip}\,|\,\mathsf{default}_{X}\,|\,c\,|\,f\,|\,x\,|\,{\rm
Phys.~{}Rev.~{}Lett.}(e)\,|\,p_{1}(e)\,|\,e\,\circ\,e\,|\,\iota_{0}(e)\,|\,\iota_{1}(e)\,|$
$\displaystyle\mathsf{elim}\,{e}\,{e}\,{e}\,|\,\lambda
x.e\,|\,e\,e\,|\,\mathsf{if}\,{\alpha}\,\mathsf{then}\,{e}\,\mathsf{else}\,{e}$

where $f$ ranges over all function symbols of $\mathrm{SL}$, $c$ are constants
in $\Lambda_{S}$, and $\alpha$ ranges over state formulas of $\mathrm{SL}$.
Typing derivations of the form $\Gamma\vdash t:X$ are given in Figure 3, where
$\Gamma$ is a set of typed variables. Note that the types of constants
$c\in\Lambda_{S}$ are also left unspecified. The type $C$ should be
interpreted as a type of commands that act on the state but don’t return any
values.

Figure 3. Typing derivations for $\mathrm{ST}+\Lambda_{S}$
$\begin{gathered}\Gamma\vdash f:D^{n}\to D\ \ \ \mbox{where $f$ has arity
$n$}\qquad\Gamma\vdash c:X\\\\[5.69054pt] \qquad\Gamma\vdash x:X\ \ \ \mbox{if
$x:X$ in $\Gamma$}\qquad\Gamma\vdash\mathsf{skip}:C\\\\[5.69054pt]
\frac{\Gamma\vdash s:X\ \ \ \Gamma\vdash t:Y}{\Gamma\vdash s\,\circ\,t:X\times
Y}\qquad\frac{\Gamma\vdash t:X\times Y}{\Gamma\vdash{\rm
Phys.~{}Rev.~{}Lett.}(t):X}\qquad\frac{\Gamma\vdash t:X\times Y}{\Gamma\vdash
p_{1}(t):Y}\\\\[5.69054pt] \frac{\Gamma\vdash
t:X}{\Gamma\vdash\iota_{0}(t):X+Y}\qquad\frac{\Gamma\vdash
t:Y}{\Gamma\vdash\iota_{1}(t):X+Y}\qquad\\\\[5.69054pt] \frac{\Gamma\vdash
r:X+Y\ \ \ \Gamma\vdash s:X\to Z\Gamma\vdash t:Y\to
Z}{\Gamma\vdash\mathsf{elim}\,{r}\,{s}\,{t}\vdash Z}\\\\[5.69054pt]
\frac{\Gamma,x:X\vdash t:Y}{\Gamma\vdash\lambda x.t:X\to
Y}\qquad\frac{\Gamma\vdash t:X\to Y\ \ \ \Gamma\vdash s:X}{\Gamma\vdash
ts:Y}\qquad\Gamma\vdash\mathsf{default}_{X}:X\\\\[5.69054pt]
\frac{\Gamma\vdash s:X\ \ \ \Gamma\vdash t:X\ \ \ \mbox{$x:D\in\Gamma$ for all
free variables of
$\alpha$}}{\Gamma\vdash\mathsf{if}\,{\alpha}\,\mathsf{then}\,{s}\,\mathsf{else}\,{t}:X}\end{gathered}$

A _denotational_ semantics of $\mathrm{ST}+\Lambda_{S}$, which is what we
require for our realizability interpretation, will be specified in detail in
Section 4 below. Operationally, the idea is that terms $t:X$ of
$\mathrm{ST}+\Lambda_{S}$ take some input state $\pi$ and evaluates to some
value $v$ and final state $\pi_{1}$ in a call-by-value way. We choose our
notation to reflect the underlying stateful computations: For example, $s\circ
t$ is used instead of what would normally be a pairing operation, because this
plays the role of simulating composition in the stateful setting. Indeed, it
will be helpful to consider a derived operator for sequential composition that
also incorporates the ‘cleanup’ seen in the examples above, and corresponds to
an instance of $\wedge_{S}I$ followed by an instance of $\wedge_{S}E_{L}$: If
$\Gamma\vdash s:C$ and $\Gamma\vdash t:X$ then $\Gamma\vdash
s\,\ast\,t:=p_{1}(s\,\circ\,t):X$. In particular, if $\Gamma\vdash t:C$ then
$\Gamma\vdash s\,\ast\,t:C$. A full exploration of the operational semantics
of $\mathrm{ST}+\Lambda_{S}$ along with correctness with respect to the
denotational semantics defined in Section 4.3 is left to future work, but we
provide some further insight in Remark 5 below, including a more detailed
discussion of the relationship between $\circ$ and pairing.

##  4\. A monadic embedding of $\mathrm{SL}$ and $\mathrm{ST}$ into a
metatheory $S^{\omega}$

We now give a semantic interpretation of both state formulas of
$\mathrm{SL}+\Delta_{H}+\Delta_{S}$ and terms in $\mathrm{ST}+\Lambda_{S}$
into a standard higher-order, many sorted logic
$S^{\omega}+\Lambda_{S^{\omega}}$.

###  4.1. The system $S^{\omega}$

This logic contains typed lambda terms along with equational axioms for
reasoning about them, together with the usual axioms and rules of many-sorted
predicate logic. Because most aspects of the logic are completely standard,
and in any case it is purely a verifying system, we are less detailed in
specifying it. Types are defined as follows:

$X::=D\,|\,1\,|\,\mathrm{Bool}\,|\,S\,|\,X\times X\,|\,X\to X$

where $D$ represents objects in the domain of $\mathrm{SL}$ (just as in
$\mathrm{ST}$), $\mathrm{Bool}$ a type of booleans, and states are now
explicitly represented as objects of type $S$. Our metatheory is an equational
calculus, with an equality symbol $=_{X}$ for all types. Typed terms include:

  * •

variables $x,y,z,\ldots$ for each type, where we denote state variables by
$\pi,\pi_{1},\pi_{2},\ldots$

  * •

a constant $f:D^{n}\to D$ for each $n$-ary function symbol of $\mathrm{SL}$,

  * •

additional, as yet unspecified constant symbols $c:X$ for interpreting objects
in $\Lambda_{S}$, along with axioms that characterise them,

  * •

a unit element $():1$ along with the axiom $x=()$,

  * •

boolean constants $\mathsf{t}$ and $\mathsf{f}$, with the axiom
$x=_{\mathrm{Bool}}\mathsf{t}\vee x=_{\mathrm{Bool}}\mathsf{f}$,

  * •

pairing $\langle{s,t}\rangle$ and projection $\mathsf{proj}_{0}(t)$,
$\mathsf{proj}_{1}(t)$ operators, with the usual axioms,

  * •

terms formed by lambda abstraction and application, with the rule $(\lambda
x.t)s=t[s/x]$,

  * •

for each type $X$ a case operator $\mathsf{case}\,{(b)}\,{(s)}\,{(t)}$ for
$b:\mathrm{Bool}$ and $s,t:X$, with axioms
$\mathsf{case}\,{\mathsf{f}}\,{x}\,{y}=x$ and
$\mathsf{case}\,{\mathsf{t}}\,{x}\,{y}=y$.

We sometimes write $x^{X}$ instead of $x:X$, and we use abbreviations such as
$\langle{x,y,z}\rangle$ for $\langle{x,\langle{y,z}\rangle}\rangle$. Atomic
formulas of $S^{\omega}$ include all ordinary predicate symbols $P,Q,R,\ldots$
of $\mathrm{SL}$ as atomic formulas, where an $n$-ary predicate $P$ in
$\mathrm{SL}$ takes arguments of type $D^{n}$ in $S^{\omega}$, along with
predicates $p,q,r,\ldots$ for each state predicate symbol of $\mathrm{SL}$,
but now, if $p$ is an $n$-ary state predicate in $\mathrm{SL}$, $p$ takes
arguments of type $D^{n}\times S$ in $S^{\omega}$. General formulas are built
using the usual logical connectives, including quantifiers for all types. The
axioms and rules of $S^{\omega}$ include the axioms of rules of predicate
logic (now in all finite types), axioms for the terms, along with the usual
equality axioms (including full extensionality). Because $S^{\omega}$ acts as
a verifying theory, we freely use strong axioms (such as extensionality),
without concerning ourselves with the minimal such system that works.

###  4.2. The embedding $[\cdot]$ on state formulas of $\mathrm{SL}$

The main purpose of our metalanguage is to allow us to reason semantically
about $\mathrm{SL}$ and $\mathrm{ST}$. To do this, we introduce an embedding
of state formulas of $\mathrm{SL}$ and terms of $\mathrm{ST}$ into
$S^{\omega}$. We use the same notation $[\cdot]$ for both, as there is no
danger of ambiguity. An informal explanation of the meaning of $[\cdot]$ on
formulas is given in Section 2.2.

An important point to highlight here is that under the semantics, the arity of
state formulas change: For any state formula $\alpha$, the interpreted formula
$[\alpha]$ now contains a single additional free variable $\pi:S$ representing
the underlying state. As mentioned earlier, state is implicit in our logic and
term languages, but needs to be made explicit under the semantics. For each
term $t$ of $\mathrm{SL}$, there is a natural interpretation of $t$ as a term
of type $D$ in $\mathrm{ST}$, namely $x\mapsto x:D$ and
$f(t_{1},\ldots,t_{n})\mapsto f(t_{1}\circ\cdots\circ t_{n}):D$. Similarly,
there is a natural interpretation of $t$ into $S^{\omega}$, this time with
$f(t_{1},\ldots,t_{n})\mapsto f(\langle{t_{1},\ldots,t_{n}}\rangle)$. We use
the same notation for $t$ in each of the three systems, as there is no risk of
ambiguity. For each _state_ formula $\alpha$ of $\mathrm{SL}$, we define a
formula $[\alpha](\pi)$ of $S^{\omega}$, whose free variables are the same as
those of $\alpha$ (but now typed with type $D$) with the potential addition of
a single state variable $\pi$, as follows:

  * •

$[\top](\pi):=\top$ and $[\bot](\pi):=\bot$,

  * •

$[p(t_{1},\ldots,t_{n})](\pi):=p(t_{1},\ldots,t_{n},\pi)$,

  * •

$[\alpha\wedge\beta](\pi):=[\alpha](\pi)\wedge[\beta](\pi)$, and similarly for
$\alpha\vee\beta$ and $\alpha\Rightarrow\beta$.

The following Lemma is easily proven using induction over propositional
derivations.

######  Lemma 2.

If $\Gamma\vdash_{H}\alpha$ in $\mathrm{SL}$ then $[\alpha](\pi)$ is provable
in $S^{\omega}$ from the assumptions $[\Gamma](\pi)$, where
$[\Gamma](\pi):=[\alpha_{1}](\pi),\ldots,[\alpha_{n}](\pi)$ for
$\Gamma:=\alpha_{1},\ldots,\alpha_{n}$. This extends to proofs in
$\mathrm{SL}+\Delta_{H}$ provided that the embedding of any axiom in
$\Delta_{H}$ is provable in $S^{\omega}+\Lambda_{S^{\omega}}$.

We are now in a position to make the semantic meaning of main formulas of
$\mathrm{SL}$ precise. Note that, technically speaking, this is not necessary
in what follows, neither to formulate our realizability interpretation nor to
prove our soundness theorem. This is because our main realizability relation
(Definition 5) is of the form $({x}\;\mathrm{sr}\;{A})$ for main formulas $A$
of $\mathrm{SL}$: This relation is basically equivalent to
$(x\,\mathrm{mr}\,[A])$ for $[A]$ as defined below and a standard modified
realizability relation mr, but our realizability interpretation essentially
acts as a simultaneous inductive definition of both standard realizability and
the embedding $[\cdot]$, and so neither of the latter need to be separately
defined.

_main_ formula $A$ of , we define a formula $[A]$ of $S^{\omega}$, whose free
variables are the same as those of $A$ (but now typed with type $D$), as
follows:

  * •

$[\top]:=\top$ and $[\bot]:=\bot$,

  * •

$[P(t_{1},\ldots,t_{n})]:=P(t_{1},\ldots,t_{n})$,

  * •

$[A\wedge B]:=[A]\wedge[B]$, $[A\vee B]:=[A]\vee[B]$ and $[\exists
x\,A]:=\exists x^{D}\,[A]$,

  * •

$[A\Rightarrow\\{{\alpha}\cdot{B}\cdot{\beta}\\}]:=[A]\Rightarrow[\\{{\alpha}\cdot{B}\cdot{\beta}\\}]$
and $[\forall x\,\\{{\alpha}\cdot{A}\cdot{\beta}\\}]:=\forall
x^{D}\,[\\{{\alpha}\cdot{A}\cdot{\beta}\\}]$

where
$[\\{{\alpha}\cdot{A}\cdot{\beta}\\}]:=\exists\pi^{S}\,[\alpha](\pi)\Rightarrow[A]\wedge\exists\pi^{\prime}\,[\beta](\pi^{\prime})$.

Similarly to Lemma 2, we can now prove the following by induction over
derivations in $\mathrm{SL}$. We omit the proof, because it is straightforward
and in any case not necessary in what follows.

######  Proposition 3.

If $\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$ in $\mathrm{SL}$ then
$[\\{{\alpha}\cdot{A}\cdot{\beta}\\}]$ is provable in $S^{\omega}$ from the
assumptions $[\Gamma]$, where $[\Gamma]:=[A_{1}],\ldots,[A_{n}]$ for
$\Gamma:=A_{1},\ldots,A_{n}$. This extends to proofs in
$\mathrm{SL}+\Delta_{H}+\Delta_{S}$ provided that the embedding of any axiom
in $\Delta_{H}$ and $\Delta_{S}$ is provable in
$S^{\omega}+\Lambda_{S^{\omega}}$.

###  4.3. The embedding $[\cdot]$ on terms of $\mathrm{ST}$

Our translation on terms is a call-by-value monadic translation using the
state monad $S\to X\times S$, which, intuitively speaking, gives a
denotational interpretation of a standard call-by-value operational semantics
of terms of $\mathrm{ST}$. A full treatment of the corresponding operational
semantics and its adequacy with respect to the and denotational semantics will
be left to future work, as we only require the latter for the realizability
interpretation. However, to help motivate the definitions that follow, and
also justify our claim that $[t]$ can be viewed as an imperative program, we
give an informal intuition in Remark 5 below.

We first define a translation on types of $\mathrm{ST}$ as follows:

  * •

$[D]:=D$, $[C]:=1$ and $[X\times Y]:=[X]\times[Y]$,

  * •

$[X+Y]:=\mathrm{Bool}\times[X]\times[Y]$

  * •

$[X\to Y]:=[X]\to S\to[Y]\times S$

######  Lemma 4.

For any type $X$ of $\mathrm{SL}$, the type $[X]$ is inhabited, in the sense
that we can define a canonical closed term $0_{X}:[X]$.

######  Proof 4.1.

Induction on types, letting $0_{D}:=c$ for a constant symbol which is assumed
to exist in $\mathrm{SL}$. The only other nonstandard case is $0_{X\to Y}$,
which can be defined as $\lambda x,\pi\,.\,\langle{0_{Y},\pi}\rangle$.

Finally, before introducing our translation on terms, we need to add
characteristic functions to $S^{\omega}$ for all state formulas (analogous to
the characteristic functions for quantifier-free formulas in [GK05]). For any
state formula $\alpha[x_{1},\ldots,x_{n}]$ of $\mathrm{SL}$, where
$x_{1},\ldots,x_{n}$ are the free variables of $\alpha$, we introduce
constants $\chi_{\alpha}\,{}\,{}\,{}\,{:}D^{n}\to S\to X\to X\to X$ satisfying
the axioms

$\displaystyle[x_{1},\ldots,x_{n}](\pi)$
$\displaystyle\Rightarrow\chi_{\alpha}\,{\langle{x_{1},\ldots,x_{n}}\rangle}\,{\pi}\,{y}\,{z}=y$
$\displaystyle[\neg\alpha][x_{1},\ldots,x_{n}](\pi)$
$\displaystyle\Rightarrow\chi_{\alpha}\,{\langle{x_{1},\ldots,x_{n}}\rangle}\,{\pi}\,{y}\,{z}=z$

For each term $\Gamma\vdash t:X$ of $\mathrm{ST}$ we define a term
$[\Gamma]\vdash[t]:S\to[X]\times S$ of $S^{\omega}$ as follows, where
$[\cdot]$ is defined on contexts as
$[x_{1}:X_{1},\ldots,x_{n}:X_{n}]:=x_{1}:[X_{1}],\ldots,x_{n}:[X_{n}]$:

  * •

$[x]\pi:=\langle{x,\pi}\rangle$,

  * •

$[\mathsf{skip}]\pi:=\langle{(),\pi}\rangle$,

  * •

$[f]\pi:=\langle{\lambda
x^{D^{n}},\pi\,.\,\langle{fx,\pi}\rangle,\pi}\rangle$,

  * •

$[c]\pi$ is appropriately defined for each additional constant in
$\Lambda_{S}$,

  * •

$[s\circ t]\pi:=\langle{a,b,\pi_{2}}\rangle$ where
$\langle{a,\pi_{1}}\rangle:=[s]\pi$ and
$\langle{b,\pi_{2}}\rangle:=[t]\pi_{1}$,

  * •

$[{\rm Phys.~{}Rev.~{}Lett.}t]\pi:=\langle{a,\pi_{1}}\rangle$ and
$[p_{1}t]\pi:=\langle{b,\pi_{1}}\rangle$ where
$\langle{a,b,\pi_{1}}\rangle:=[t]\pi$,

  * •

$[\iota_{0}t]\pi:=\langle{\mathsf{f},a,0_{Y},\pi_{1}}\rangle$ and
$[\iota_{1}t]:=\langle{\mathsf{t},0_{X},b,\pi_{1}}\rangle$ for
$\langle{a,\pi_{1}}\rangle:=[t]\pi$,

  * •

$[\mathsf{elim}\,{r}\,{s}\,{t}]\pi:=\mathsf{case}\,{e}\,{(fa\pi_{2})}\,{(gb\pi_{3})}$
for $\langle{e,a,b,\pi_{1}}\rangle:=[r]\pi$,
$\langle{f,\pi_{2}}\rangle:=[s]\pi_{1}$,
$\langle{g,\pi_{3}}\rangle:=[t]\pi_{1}$,

  * •

$[\lambda x.t]\pi:=\langle{\lambda x^{[X]}.[t],\pi}\rangle$,

  * •

$[ts]\pi:=fa\pi_{2}$ for $\langle{f,\pi_{1}}\rangle:=[t]\pi$ and
$\langle{a,\pi_{2}}\rangle:=[s]\pi_{1}$,

  * •

$[\mathsf{default}_{X}]\pi:=\langle{0_{X},\pi}\rangle$,

  * •

$[\mathsf{if}\,{\alpha[x_{1},\ldots,x_{n}]}\,\mathsf{then}\,{s}\,\mathsf{else}\,{t}]\pi:=\chi_{\alpha}\,{\langle{x_{1},\ldots,x_{n}}\rangle}\,{\pi}\,{([s]\pi)}\,{([t]\pi)}$
where $\\{x_{1},\ldots,x_{n}\\}$ are the free variables of $\alpha$.

######  Remark 5.

The intuition behind the embedding $[t]$ is to give a denotational semantics
for $t$ as a stateful program. Informally, a term $t:X$ of $\mathrm{ST}$ would
have operational behaviour
$\langle{t,\pi}\rangle\Downarrow\langle{v,\pi_{1}}\rangle$, where we imagine
that $t$ in state $\pi$ evaluates to a value $v$ and returns a state
$\pi_{1}$. We view $[X]$ as the set of denotations of values of type $X$, and
$[t]:S\to[X]\times S$ accordingly as a function with
$[t]\pi=\langle{[v],\pi_{1}}\rangle$. The interpretation of fully typed terms
$[\Gamma\vdash t:X]$ correspond to mappings $[\Gamma]\to S\to[X]\times S$
where free variables of $t$ can be instantiated by values of the corresponding
type.

With this intuition in mind, each component of Definition 4.3 corresponds to a
natural _operational_ interpretation of the corresponding term forming rule.
For example, the intended operational semantics of $s\circ t$ would be

$\frac{\langle{s,\pi}\rangle\Downarrow\langle{u,\pi_{1}}\rangle\ \ \
\langle{t,\pi_{1}}\rangle\Downarrow\langle{v,\pi_{2}}\rangle}{\langle{s\,\circ\,t,\pi}\rangle\Downarrow\langle{\langle{u,v}\rangle,\pi_{2}}\rangle}$

and this behaviour is embodied by the denotation $[s\,\circ\,t]$, which maps
$\pi$ to $\langle{a,b,\pi_{2}}\rangle$ where $a$ can be interpreted as the
denotation of the value $u$, and $b$ as the denotation of $v$. Similarly, the
call-by-value operational semantics of function application would be expressed
by the rule

$\frac{\langle{t,\pi}\rangle\Downarrow\langle{u,\pi_{1}}\rangle\ \ \
\langle{s,\pi_{1}}\rangle\Downarrow\langle{v,\pi_{2}}\rangle\ \ \
\langle{uv,\pi_{2}}\rangle\Downarrow\langle{w,\pi_{3}}\rangle}{\langle{ts,\pi}\rangle\Downarrow\langle{w,\pi_{3}}\rangle}$

i.e. we evaluate first the function $t$, then the argument $s$, then the
function application itself. This order of evaluation along with the behaviour
of the state is represented semantically by $[ts]$. Finally, we note that the
main interactions with the state for terms of $\mathrm{ST}+\Lambda_{S}$ are
driven by the constants $c\in\Lambda_{S}$, whose semantic interpretation as
stateful programs will need to be specified in each case.

Our monadic semantics and its relationship with the intended call-by-value
operational semantics is very similar in spirit to the monadic denotational
semantics used in [DLR15] and related papers (but with the state monad instead
of the complexity monad). We leave a formal definition and detailed
exploration of the operational semantics of extracted imperative programs to
future work, where it is anticipated that existing work on the operational
semantics of imperative languages could be useful and revealing (e.g. [CLM13,
McC10, Red96]), particularly in extending our realizability interpretation to
incorporate richer imperative languages.

The following lemmas will be useful when verifying our realizability
interpretation in the next section. The first is by a simple induction on
terms.

######  Lemma 6.

For any term $t$ of $\mathrm{SL}$, we have $[t]\pi=\langle{t,\pi}\rangle$ (cf.
Definitions 4.2 and 4.3).

######  Lemma 7 (Currying in $\mathrm{ST}$).

Suppose that $\Gamma,x:X,y:Y\vdash t:Z$ is a term in $\mathrm{ST}$, and define
$\Gamma\vdash\lambda^{\ast}v.t:X\times Y\to Z$ by $\lambda^{\ast}v.t:=\lambda
v.(\lambda x,y.t)({\rm Phys.~{}Rev.~{}Lett.}v)(p_{1}v)$ where $v$ is not free
in $t$. Then for any $s:X\times Y$ we have

$[(\lambda^{\ast}v.t)s]\pi=[t][a/x,b/y]\pi_{1}$

where $\langle{a,b,\pi_{1}}\rangle:=[s]\pi$.

######  Proof 4.2.

By unwinding the definition of $[\cdot]$. For any variable $v:X\times Y$ we
have $[{\rm Phys.~{}Rev.~{}Lett.}v]\pi=\langle{\mathsf{proj}_{0}v,\pi}\rangle$
and $[p_{1}v]\pi=\langle{\mathsf{proj}_{1}v,\pi}\rangle$, and we also have
$[\lambda x,y\,.\,t]\pi=\langle{\lambda x,\pi.\langle{\lambda
y.[t],\pi}\rangle,\pi}\rangle$. We therefore calculate

$[(\lambda x,y.t)({\rm Phys.~{}Rev.~{}Lett.}v)]\pi=(\lambda
x,\pi.\langle{\lambda
y.[t],\pi}\rangle)(\mathsf{proj}_{0}v)\pi=\langle{\lambda
y.[t][\mathsf{proj}_{0}v/x],\pi}\rangle$

and thus

$[(\lambda x,y.t)({\rm Phys.~{}Rev.~{}Lett.}v)(p_{1}v)]\pi=(\lambda
y.[t][\mathsf{proj}_{0}v/x])(\mathsf{proj}_{1}v)\pi=[t][\mathsf{proj}_{0}v/x,\mathsf{proj}_{1}v/y]\pi$

Finally, we can see that if $\langle{a,b,\pi_{1}}\rangle:=[s]\pi$ then

$\displaystyle\pi$ $\displaystyle=(\lambda v.[(\lambda x,y.t)({\rm
Phys.~{}Rev.~{}Lett.}v)(p_{1}v)])(\langle{a,b}\rangle)\pi_{1}$
$\displaystyle=(\lambda
v.[t][\mathsf{proj}_{0}v/x,\mathsf{proj}_{1}v/y])(\langle{a,b}\rangle)\pi_{1}$
$\displaystyle=[t][\mathsf{proj}_{0}v/x,\mathsf{proj}_{1}v/y][\langle{a,b}\rangle/v]\pi_{1}$
$\displaystyle=[t][a/x,b/y]\pi_{1}$

which completes the proof.

##  5\. A realizability interpretation of $\mathrm{SL}$ into $\mathrm{ST}$

We now come to the main contribution of the paper, which is the definition of
a realizability relation between terms of $\mathrm{ST}$ and formulas of
$\mathrm{SL}$, along with a soundness theorem that shows us how to extract
realizers from proofs. Our metatheory $S^{\omega}$ is used to define the
realizability relation and prove the soundness theorem. [Types of realizers]
To each main formula $A$ of $\mathrm{SL}$ we assign a type $\tau_{S}({A})$ of
$\mathrm{ST}$ as follows:

  * •

$\tau_{S}({\top})=\tau_{S}({\bot})=\tau_{S}({P(t_{1},\ldots,t_{n})}):=C$,

  * •

$\tau_{S}({A\wedge B}):=\tau_{S}({A})\times\tau_{S}({B})$,

  * •

$\tau_{S}({A\vee B}):=\tau_{S}({A})+\tau_{S}({B})$,

  * •

$\tau_{S}({\exists x\,A}):=D\times\tau_{S}({A})$,

  * •

$\tau_{S}({A\Rightarrow\\{{\alpha}\cdot{B}\cdot{\beta}\\}}):=\tau_{S}({A})\to\tau_{S}({B})$,

  * •

$\tau_{S}({\forall
x\,\\{{\alpha}\cdot{A}\cdot{\beta}\\}}):=D\to\tau_{S}({A})$.

[Realizability relation] For each main formula $A$ of $\mathrm{SL}$ we define
a formula ${x}\;\mathrm{sr}\;{A}$ of $S^{\omega}$, whose free variables are
contained in those of $A$ (now typed with type $D$) together with a fresh
variable $x:[\tau_{S}({A})]$, by induction on the structure of $A$ as follows:

  * •

${x}\;\mathrm{sr}\;{Q}:=Q$ for $Q=\top,\bot$ or $P(t_{1},\ldots,t_{n})$,

  * •

${x}\;\mathrm{sr}\;{A\wedge
B}:=({\mathsf{proj}_{0}x}\;\mathrm{sr}\;{A})\wedge({\mathsf{proj}_{1}x}\;\mathrm{sr}\;{B})$,

  * •

${x}\;\mathrm{sr}\;{A\vee
B}:=(\mathsf{proj}_{0}x=\mathsf{f}\Rightarrow{\mathsf{proj}_{0}(\mathsf{proj}_{1}x)}\;\mathrm{sr}\;{A})\wedge(\mathsf{proj}_{0}x=\mathsf{t}\Rightarrow{\mathsf{proj}_{1}(\mathsf{proj}_{1}x)}\;\mathrm{sr}\;{B})$,

  * •

${x}\;\mathrm{sr}\;{\exists
y\,A(y)}:=({\mathsf{proj}_{1}x}\;\mathrm{sr}\;{A})[\mathsf{proj}_{0}x/y]$,

  * •

${f}\;\mathrm{sr}\;{(A\Rightarrow\\{{\alpha}\cdot{B}\cdot{\beta}\\})}:=\forall
x^{[\tau_{S}({A})]}\,({x}\;\mathrm{sr}\;{A}\Rightarrow{fx}\;\mathrm{sr}\;{\\{{\alpha}\cdot{B}\cdot{\beta}\\}})$,

  * •

${f}\;\mathrm{sr}\;{(\forall
x\,\\{{\alpha(x)}\cdot{A(x)}\cdot{\beta(x)}\\})}:=\forall
x^{D}\,({fx}\;\mathrm{sr}\;{\\{{\alpha(x)}\cdot{A(x)}\cdot{\beta(x)}\\}})$,

where for $x:S\to[\tau_{S}({A})]\times S$ we define

  * •

${x}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\beta}\\}}:=\forall\pi^{S}\,([\alpha](\pi)\Rightarrow{\mathsf{proj}_{0}(x\pi)}\;\mathrm{sr}\;{A}\wedge[\beta](\mathsf{proj}_{1}(x\pi)))$.

The following substitution lemma is easily proven by induction on formulas of
$\mathrm{SL}$.

######  Lemma 8.

For any term $t$ of $\mathrm{SL}$ and $s:[\tau_{S}({A})]$ we have
${s}\;\mathrm{sr}\;{A[t/x]}=({s}\;\mathrm{sr}\;{A})[t/x]$, where $x$ is not
free in $s$ and on the right hand side we implicitly mean the natural
interpretation of $t$ in $S^{\omega}$ (cf. Definition 4.2).

######  Theorem 9 (Soundness).

Suppose that

$\Gamma:=A_{1}^{u_{1}},\ldots,A_{n}^{u_{n}}\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\beta}\\}$

is provable in $\mathrm{SL}$. Then we can extract from the proof a term
$\Delta,\tau_{S}({\Gamma})\vdash t:\tau_{S}({A})$ of $\mathrm{ST}$, where
$\Delta$ contains the free variables of $\Gamma$ and
$\\{{\alpha}\cdot{A}\cdot{\beta}\\}$ (typed with type $D$) and
$\tau_{S}({\Gamma}):=x_{1}:\tau_{S}({A_{1}}),\ldots,x_{n}:\tau_{S}({A_{n}})$
for fresh variables $x_{1},\ldots,x_{n}$, such that the formula

${[t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\beta}\\}}$

is provable in $S^{\omega}$ from the assumptions
$({x_{1}}\;\mathrm{sr}\;{A_{1}})^{u_{1}},\ldots,({x_{n}}\;\mathrm{sr}\;{A_{n}})^{u_{n}}$
for $x_{i}:[\tau_{S}({A_{i}})]$. The theorem holds more generally for proofs
in $\mathrm{SL}+\Delta_{H}+\Delta_{S}$, now provably in
$S^{\omega}+\Lambda_{S^{\omega}}$, if:

  * •

for any axiom $\Gamma\vdash_{H}\alpha$ in $\Delta_{H}$, the corresponding
axiom $[\Gamma](\pi)\Rightarrow[\alpha](\pi)$ is added to
$\Lambda_{S^{\omega}}$,

  * •

for any axiom in $\Delta_{S}$ there is a term $t$ of $\mathrm{ST}+\Lambda_{S}$
such that $[t]$ realizes that axiom provably in
$S^{\omega}+\Lambda_{S^{\omega}}$.

######  Proof 5.1.

Induction on the structure of derivations in $\mathrm{SL}$. In all cases, we
assume as global assumptions
$({x_{1}}\;\mathrm{sr}\;{A_{1}})^{u_{1}},\ldots,({x_{n}}\;\mathrm{sr}\;{A_{n}})^{u_{n}}$,
and our aim is then to produce a term $t$ such that if $[\alpha](\pi)$ holds
for some state variable $\pi$, then ${a}\;\mathrm{sr}\;{A}$ and
$[\beta](\pi_{1})$ hold for $\langle{a,\pi_{1}}\rangle:=[t]\pi$.

  * •

For the axiom $\Gamma\vdash_{S}\\{{\alpha}\cdot{A}\cdot{\alpha}\\}$, if
$A^{u}\in\Gamma$ we define $t:=x$ for the corresponding variable
$x:\tau_{S}({A})$. Then $[x]\pi:=\langle{x,\pi}\rangle$ for
${x}\;\mathrm{sr}\;{A}$ and $[\alpha](\pi)$. For
$\Gamma\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\alpha}\\}$ we define
$t:=\mathsf{skip}$ and the verification is even simpler.

  * •

($\wedge_{S}I$) Given terms $s,t$ with
${[s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\beta}\\}}$ and
${[t]}\;\mathrm{sr}\;{\\{{\beta}\cdot{B}\cdot{\gamma}\\}}$, from
$[\alpha](\pi)$ we can infer ${a}\;\mathrm{sr}\;{A}$ and $[\beta](\pi_{1})$
for $\langle{a,\pi_{1}}\rangle:=[s]\pi$, and from $[\beta](\pi_{1})$ it
follows that ${b}\;\mathrm{sr}\;{B}$ and $[\gamma](\pi_{2})$ for
$\langle{b,\pi_{2}}\rangle:=[t]\pi_{1}$, therefore we have shown that
${[s\circ t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A\wedge B}\cdot{\gamma}\\}}$.

  * •

($\wedge_{S}E_{i}$) If ${[t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A\wedge
B}\cdot{\beta}\\}}$ then ${\langle{a,b}\rangle}\;\mathrm{sr}\;{A\wedge B}$ and
$[\beta](\pi_{1})$ follow from $[\alpha](\pi)$, where
$\langle{a,b,\pi_{1}}\rangle:=[t]\pi$. But then ${[{\rm
Phys.~{}Rev.~{}Lett.}t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\beta}\\}}$
and ${[p_{1}t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{B}\cdot{\beta}\\}}$.

  * •

($\vee_{S}I_{i}$) If
${[t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\beta}\\}}$ and $[\alpha](\pi)$
holds, then ${a}\;\mathrm{sr}\;{A}$ and $[\beta](\pi_{1})$ for
$\langle{a,\pi_{1}}\rangle:=[t]\pi$, and therefore

$(b=\mathsf{f}\Rightarrow{a}\;\mathrm{sr}\;{A})\wedge(b=\mathsf{t}\Rightarrow{0_{\tau_{S}({B})}}\;\mathrm{sr}\;{B})$

for $b:=\mathsf{f}$. Thus ${[\iota_{0}t]}\;\mathrm{sr}\;{A\vee B}$. By an
entirely analogous argument we can show that
${[\iota_{1}t]}\;\mathrm{sr}\;{A\vee B}$ whenever ${[t]}\;\mathrm{sr}\;{B}$.

  * •

($\vee_{S}E$) Suppose that $r$, $s(x)$ and $t(y)$ are such that
${[r]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A\vee B}\cdot{\beta}\\}}$,
${[s](x)}\;\mathrm{sr}\;{\\{{\beta}\cdot{C}\cdot{\gamma}\\}}$ assuming
${x}\;\mathrm{sr}\;{A}$, and
${[t](y)}\;\mathrm{sr}\;{\\{{\beta}\cdot{C}\cdot{\gamma}\\}}$ assuming
${y}\;\mathrm{sr}\;{B}$. We claim that

${[\mathsf{elim}\,{r}\,{(\lambda x.s)}\,{(\lambda
y.t)}]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{C}\cdot{\gamma}\\}}$

To prove this, first note that if $[\alpha](\pi)$, we have
${\langle{e,a,b}\rangle}\;\mathrm{sr}\;{A\vee B}$ and $[\beta](\pi_{1})$ for
$\langle{e,a,b,\pi_{1}}\rangle:=[r]\pi$. There are now two possibilities. If
$e=\mathsf{f}$ then

$\displaystyle\pi$ $\displaystyle=fa\pi_{2}\ \ \ \mbox{for
$\langle{f,\pi_{2}}\rangle:=[\lambda x.s]\pi_{1}=\langle{\lambda
x.[s](x),\pi_{1}}\rangle$}$ $\displaystyle=(\lambda x.[s](x))a\pi_{1}$
$\displaystyle=[s](a)\pi_{1}$

But since $[\beta](\pi_{1})$ holds and $e=\mathsf{f}$ also implies that
${a}\;\mathrm{sr}\;{A}$, we have ${c}\;\mathrm{sr}\;{C}$ and
$[\gamma](\pi_{2})$ for $\langle{c,\pi_{2}}\rangle:=[s](a)\pi_{1}$, which
proves the main claim in the case $e=\mathsf{f}$. An analogous argument works
for the case $e=\mathsf{t}$.

  * •

($\Rightarrow_{S}I$) If $t(x)$ is such that
${[t](x)}\;\mathrm{sr}\;{\\{{\alpha}\cdot{B}\cdot{\beta}\\}}$ whenever
${x}\;\mathrm{sr}\;{A}$, then by definition we have

${\lambda
x.[t]}\;\mathrm{sr}\;{A\Rightarrow\\{{\alpha}\cdot{B}\cdot{\beta}\\}}$

and therefore ${[\lambda
x.t]}\;\mathrm{sr}\;{\\{{\gamma}\cdot{A\Rightarrow\\{{\alpha}\cdot{B}\cdot{\beta}\\}}\cdot{\gamma}\\}}$
for any $\gamma$.

  * •

($\Rightarrow_{S}E$) Assume that
${[s]}\;\mathrm{sr}\;{\\{{\beta}\cdot{A}\cdot{\gamma}\\}}$ and
${[t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A\Rightarrow\\{{\gamma}\cdot{B}\cdot{\delta}\\}}\cdot{\beta}\\}}$.
If $[\alpha](\pi)$ holds then defining $\langle{f,\pi_{1}}\rangle:=[t]\pi$ we
have $[\beta]\pi_{1}$ and

${x}\;\mathrm{sr}\;{A}\Rightarrow{fx}\;\mathrm{sr}\;{\\{{\gamma}\cdot{B}\cdot{\delta}\\}}$

Similarly, defining $\langle{a,\pi_{2}}\rangle:=[s]\pi_{1}$, it follows that
$[\gamma](\pi_{2})$ and ${a}\;\mathrm{sr}\;{A}$. Finally, setting
$\langle{b,\pi_{3}}\rangle:=fa\pi_{2}$ it follows that ${b}\;\mathrm{sr}\;{B}$
and $[\delta](\pi_{3})$, and we have therefore proven that
${[ts]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{B}\cdot{\delta}\\}}$.

  * •

($\bot_{S}E$) If ${[t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{\bot}\cdot{\beta}\\}}$
then from $[\alpha](\pi)$ we can infer ${a}\;\mathrm{sr}\;{\bot}$ and
$[\beta](\pi_{2})$ for $\langle{a,\pi_{1}}\rangle:=[t]\pi$. But
${a}\;\mathrm{sr}\;{\bot}=\bot$, and from $\bot$ we can deduce anything, and
in particular ${0_{\tau_{S}({A})}}\;\mathrm{sr}\;{A}$ and $[\gamma](\pi)$,
from which it follows that
${[\mathsf{default}_{\tau_{S}({A})}]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\gamma}\\}}$.

  * •

($\forall_{S}I$) Suppose that $t(x)$ is such that
${[t](y)}\;\mathrm{sr}\;{\\{{\alpha[y/x]}\cdot{A[y/x]}\cdot{\beta[y/x]}\\}}$,
where $y\equiv x$ or $y$ is not free in $\\{{\alpha}\cdot{A}\cdot{\beta}\\}$,
and $y$ is not free in $\Gamma$. Then since $y$ is not free in any of the
assumptions ${x_{i}}\;\mathrm{sr}\;{A_{i}}$, we can deduce in $S^{\omega}$
that

$\forall x^{D}\,{[t](x)}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\beta}\\}}$

and therefore ${\lambda x.[t]}\;\mathrm{sr}\;{\forall
x\,\\{{\alpha}\cdot{A}\cdot{\beta}\\}}$, and thus (just as for
$\Rightarrow_{S}I$) we have

${[\lambda x.t]}\;\mathrm{sr}\;{\\{{\gamma}\cdot{\forall
x\,\\{{\alpha}\cdot{A}\cdot{\beta}\\}}\cdot{\gamma}\\}}$

for any $\gamma$.

  * •

($\forall_{S}E$) Suppose that ${[s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{\forall
x\,\\{{\beta}\cdot{A}\cdot{\gamma}\\}}\cdot{\beta[t/x]}\\}}$ and that
$[\alpha](\pi)$ holds. Then we have ${f}\;\mathrm{sr}\;{\forall
x\,\\{{\beta}\cdot{A}\cdot{\gamma}\\}}$ and $[\beta][t/x](\pi_{1})$ for
$\langle{f,\pi}\rangle:=[s]\pi$. Now, using Lemma 6 we have
$[st]\pi=ft\pi_{1}$ for the natural interpretation of $t$ in $S^{\omega}$,
since we can prove in $S^{\omega}$ that

${ft}\;\mathrm{sr}\;{\\{{\beta[t/x]}\cdot{A[t/x]}\cdot{\gamma[t/x]}\\}}$

it follows that ${a}\;\mathrm{sr}\;{A[t/x]}$ and $[\gamma][t/x](\pi_{2})$ for
$\langle{a,\pi_{2}}\rangle:=ft\pi_{1}$, and therefore we have shown that
${[st]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A[t/x]}\cdot{\gamma[t/x]}\\}}$.

  * •

($\exists_{S}I$) If
${[s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A[t/x]}\cdot{\beta}\\}}$ and
$[\alpha](\pi)$ then ${a}\;\mathrm{sr}\;{A[t/x]}$ and $[\beta](\pi_{1})$ for
$\langle{a,\pi_{1}}\rangle:=[s]\pi$. By Lemma 8 we therefore have
$({a}\;\mathrm{sr}\;{A})[t/x]$, and therefore
${\langle{t,a}\rangle}\;\mathrm{sr}\;{\exists x\,A}$. Observing (using Lemma
6) that $[t\circ s]\pi=\langle{t,a,\pi_{1}}\rangle$, we have shown that
${[t\circ s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{\exists x\,A}\cdot{\beta}\\}}$.

  * •

($\exists_{S}E$) Suppose that $s$ and $t(x,z)$ are such that
${[s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{\exists x\,A}\cdot{\beta}\\}}$ and

${z}\;\mathrm{sr}\;{A[y/x]}\Rightarrow{[t](y,z)}\;\mathrm{sr}\;{\\{{\beta}\cdot{C}\cdot{\gamma}\\}}$

where $y\equiv x$ or $y$ is not free in $A$, and $y$ is also not free in $C$,
$\alpha$, $\beta$, $\gamma$ or $\Gamma$. By Lemma 8 that
${z}\;\mathrm{sr}\;{A[y/x]}=({z}\;\mathrm{sr}\;{A})[y/x]={\langle{y,z}\rangle}\;\mathrm{sr}\;{\exists
x\,A}$ we therefore have

${\langle{y,z}\rangle}\;\mathrm{sr}\;{\exists
x\,A}\Rightarrow{[t](y,z)}\;\mathrm{sr}\;{\\{{\beta}\cdot{C}\cdot{\gamma}\\}}$

Now, applying Lemma 7 to $\Delta,\Gamma,y:D,z:\tau_{S}({A})\vdash
t:\tau_{S}({C})$, we have

$[(\lambda^{\ast}v.t)s]\pi=[t](e,a)\pi_{1}$

for $\langle{e,a,\pi_{1}}\rangle:=[s]\pi$. Now, if $[\alpha](\pi)$ holds, then
we have ${\langle{e,a}\rangle}\;\mathrm{sr}\;{\exists x\,A}$ and
$[\beta](\pi_{1})$, and therefore since
${[t](e,a)}\;\mathrm{sr}\;{\\{{\beta}\cdot{C}\cdot{\gamma}\\}}$, we have
${c}\;\mathrm{sr}\;{C}$ and $[\gamma](\pi_{2})$ for
$\langle{c,\pi_{2}}\rangle=[t](e,a)\pi_{1}=[(\lambda^{\ast}v.t)s]\pi$, and
thus we have shown that
${[(\lambda^{\ast}v.t)s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{C}\cdot{\gamma}\\}}$.

  * •

($cons$) If $\alpha\vdash_{H}\beta$ and $\gamma\vdash_{H}\delta$ then by Lemma
2 both $[\alpha](\pi)\Rightarrow[\beta](\pi)$ and
$[\gamma](\pi)\Rightarrow[\delta](\pi)$ are provable in $S^{\omega}$
(respectively $S^{\omega}+\Lambda_{S^{\omega}}$ for the general version of the
theorem) for any $\pi:S$. It is then easy to show that if
${[t]}\;\mathrm{sr}\;{\\{{\beta}\cdot{A}\cdot{\gamma}\\}}$ then we also have
${[t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\delta}\\}}$.

  * •

($cond$) Suppose that
${[s]}\;\mathrm{sr}\;{\\{{\alpha\wedge\gamma}\cdot{A}\cdot{\delta}\\}}$ and
${[t]}\;\mathrm{sr}\;{\\{{\beta\wedge\gamma}\cdot{A}\cdot{\delta}\\}}$. We
claim that

${[\mathsf{if}\,{\alpha}\,\mathsf{then}\,{s}\,\mathsf{else}\,{t}]}\;\mathrm{sr}\;{\\{{\gamma}\cdot{A}\cdot{\delta}\\}}$

To prove this, suppose that $[\gamma](\pi)$ holds. Since
$\vdash_{H}\alpha\vee\beta$ then $[\alpha](\pi)\vee[\beta](\pi)$ is provable
in $S^{\omega}$, and so we consider two cases. Let $\\{x_{1},\ldots,x_{n}\\}$
be the free variables of $\alpha$. If $[\alpha](\pi)$ holds, then

$[\mathsf{if}\,{\alpha}\,\mathsf{then}\,{s}\,\mathsf{else}\,{t}]\pi=\chi_{\alpha}\,{\langle{x_{1},\ldots,x_{n}}\rangle}\,{\pi}\,{([s]\pi)}\,{([t]\pi)}=[s]\pi$

and since then $[\alpha](\pi)\wedge[\gamma](\pi)$ we have
${a}\;\mathrm{sr}\;{A}$ and $[\delta](\pi_{1})$ for
$\langle{a,\pi_{1}}\rangle:=[s]\pi$. On the other hand, if $[\beta](\pi)$
holds, then by an analogous argument we can show that ${a}\;\mathrm{sr}\;{A}$
and $[\delta](\pi_{1})$ for
$\langle{a,\pi_{1}}\rangle:=[t]\pi=[\mathsf{if}\,{\alpha}\,\mathsf{then}\,{s}\,\mathsf{else}\,{t}]\pi$,
and we are done.

The extension of the soundness theorem to $\mathrm{SL}+\Delta_{H}+\Delta_{S}$
is straightforward, as the soundness proof is modular and so any axioms along
with their realizers can be added. The first condition is needed so that Lemma
2 (needed for the $cons$ rule) continues to apply.

For the free variable condition that the free variables of $t$ are contained
in those of $\Gamma$, $\\{{\alpha}\cdot{A}\cdot{\beta}\\}$ and
$\tau_{S}({\Gamma})$, if this were not the case, we could simply ground those
variables with a canonical constant $c:D$ and we would still have
${\tilde{t}}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A}\cdot{\beta}\\}}$ for the
resulting term $\tilde{t}$.

######  Corollary 10 (Program extraction).

Suppose that the sentence

$\vdash_{S}\\{{\alpha}\cdot{\forall x\,\\{{\beta}\cdot{\exists
y\,P(x,y)}\cdot{\gamma(x)}\\}}\cdot{\beta}\\}$

is provable in $\mathrm{SL}+\Delta_{S}$. Then we can extract a closed
realizing term $t:D\to D\times C$ in $\mathrm{ST}+\Lambda_{S}$ such that
defining $g:D\to S\to D\times S$ by $gx\pi:=\langle{a,\pi_{2}}\rangle$ for
$\langle{f,\pi_{1}}\rangle:=[t]\pi$ and
$\langle{a,(),\pi_{2}}\rangle:=fx\pi_{1}$, we have

$\forall\pi^{S}([\alpha](\pi)\Rightarrow\forall
x^{D}\,(P(x,\mathsf{proj}_{0}(gx\pi))\wedge[\gamma](x)(\mathsf{proj}_{1}(gx\pi))))$

provably in $S^{\omega}+\Lambda_{S^{\omega}}$.

###  5.1. Simplification and removal of unit types

In presentations of modified realizability that use product types instead of
type sequences, it is common to introduce the notion of a Harrop formula (a
formula that does not contain disjunction or existential quantification in a
positive position) and define realizability in a way that all Harrop formulas
have unit realizability type, so that e.g. $\tau_{S}({\forall x\,(P\wedge
Q)})=1$ for atomic predicates $P$ and $Q$, rather than $\tau_{S}({\forall
x\,(P\wedge Q)})=D\to 1\times 1$ as for us. We have avoided this
simplification earlier on, as it would have added additional cases and
bureaucracy to our soundness theorem. However, we can compensate retroactively
for this choice by introducing equivalences on types that eliminate unit
types, namely the closure under contexts of

$1\times X\simeq X\simeq X\times 1\ \ \ (1\to X)\simeq X\ \ \ (X\to 1)\simeq
1$

along with corresponding equivalences on terms, also closed under contexts:

$t^{1\times X}\simeq\mathsf{proj}_{1}(t)^{X}\ \ \ t^{X\times
1}\simeq\mathsf{proj}_{0}(t)^{X}\ \ \ t^{1\to X}\simeq t()\ \ \
t^{X}\simeq\lambda x^{1}.t\ \ \ t^{X\to 1}\simeq()$

For example, in Corollary 10 we would then have

$[t]\pi:(D\to S\to D\times 1\times S)\times S\simeq(D\to S\to D\times S)\times
S\ \ \ \mbox{and}\ \ \ gx\pi\simeq fx\pi_{1}.$

For us, the equivalence relation $\simeq$ will not play a formal role in the
paper, but will be used to provide simplified descriptions of extracted
programs. In particular, we do not rely on it in any way for the main results.
To incorporate the simplifications formally into our framework, the most
obvious route would involve defining a more elaborate realizability relation
as indicated above, with the interpretation of Harrop formulas treated
separately (as in the recent and related paper [BT21]), which would then also
generate many new (but routine) cases in the soundness proof. Given that we
are already introducing a new and nonstandard realizability relation, in this
article we prefer to work with a simple interpretation and use the
equivalences above in an informal way to more concisely describe the meaning
of extracted programs.

###  5.2. Examples of program extraction

We now continue the short illustrative examples we outlined in Section 2.2.

[Simple read-write] In Example 2.2 we considered a state where three actions
were possible (writing to the state, performing a calculation, and reading the
output from the state). We can formalise these three actions semantically in
the metatheory $S^{\omega}$ by including three constants in
$\Lambda_{S^{\omega}}$, namely $c_{1}:D\to S\to S$, $c_{2}:S\to S$ and
$c_{3}:S\to D$, along with the characterising axioms:

  1. (1)

$\mathsf{query}(x,c_{1}x\pi)$,

  2. (2)

$\mathsf{query}(x,\pi)\Rightarrow\mathsf{return}_{P}(x,c_{2}\pi)$,

  3. (3)

$\mathsf{return}_{P}(x,\pi)\Rightarrow P(x,c_{3}\pi)$.

While we are able to use these constants to form terms in $S^{\omega}$ such as
$\lambda\pi,\pi_{1},x\,.\,\langle{c_{1}x\pi,c_{2}\pi_{1}}\rangle$, which could
be viewed as non-sequential in the sense that we take two input states as
arguments, we can force them to be applied in a sequential, call-by-value
manner by adding three corresponding constants to our term calculus
$\mathrm{ST}$, namely including $\mathsf{write}:D\to C$, $\mathsf{calc}:C$ and
$\mathsf{read}:D\times C$ in $\Lambda_{S}$, along with the embedding rules

  * •

$[\mathsf{write}]\pi:=\langle{\lambda
x,\pi^{\prime}\,.\,\langle{(),c_{1}x\pi^{\prime}}\rangle,\pi}\rangle\simeq\langle{c_{1},\pi}\rangle$,

  * •

$[\mathsf{calc}]\pi:=\langle{(),c_{2}\pi}\rangle$ so that
$[\mathsf{calc}]\simeq c_{2}$,

  * •

$[\mathsf{read}]\pi:=\langle{c_{3}\pi,(),\pi}\rangle\simeq\langle{c_{3}\pi,\pi}\rangle$.

and then restricting out attention to terms of the form $[t]$ for
$t\in\mathrm{ST}+\\{\mathsf{write},\mathsf{calc},\mathsf{read}\\}$. We can
then prove the following in $S^{\omega}$ i.e. that all axioms in $\Delta_{S}$
can be realised:

  * •

${[\mathsf{write}(x)]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{\top}\cdot{\mathsf{query}(x)}\\}}$,

  * •

${[\mathsf{calc}]}\;\mathrm{sr}\;{\\{{\mathsf{query}(x)}\cdot{\top}\cdot{\mathsf{return}_{P}(x)}\\}}$,

  * •

${[\mathsf{read}]}\;\mathrm{sr}\;{\\{{\mathsf{return}_{P}(x)}\cdot{\exists
y\,P(x,y)}\cdot{\top}\\}}$.

and thus Theorem 9 applies to $\mathrm{SL}+\Delta_{H}+\Delta_{S}$ for
$\Delta_{H}=\emptyset$. In particular, we have

${[t]}\;\mathrm{sr}\;{\\{{\beta}\cdot{\forall x\,\\{{\alpha}\cdot{\exists
y\,P(x,y)}\cdot{\top}\\}}\cdot{\beta}\\}}$

for $t:=\lambda
x\,.\,((\mathsf{write}(x)\,\ast\,\mathsf{calc})\,\ast\,\mathsf{read})$ where
$\,\ast\,$ is sequential composition operator from Definition 3. A formal
derivation of this term from the corresponding proof given in Example 2.2 is
as follows:

$x:D\vdash\mathsf{write}(x):C$$x:D\vdash\mathsf{calc}:C$
$\;\scriptstyle\wedge_{S}I$
$x:D\vdash\mathsf{write}(x)\circ\mathsf{calc}:C\times C$
$\;\scriptstyle\wedge_{S}E_{L}$
$x:D\vdash\mathsf{write}(x)\,\ast\,\mathsf{calc}:C$
$x:D\vdash\mathsf{read}:D\times C$ $\;\scriptstyle\wedge_{S}I$
$x:D\vdash(\mathsf{write}(x)\,\ast\,\mathsf{calc})\circ\mathsf{read}:C\times
D\times C$ $\;\scriptstyle\wedge_{S}E_{L}$
$x:D\vdash(\mathsf{write}(x)\,\ast\,\mathsf{calc})\,\ast\,\mathsf{read}:D\times
C$ $\;\scriptstyle\forall_{S}I$ $\vdash\lambda
x\,.\,((\mathsf{write}(x)\,\ast\,\mathsf{calc})\,\ast\,\mathsf{read}):D\to
D\times C$

[Fixed-length array sorting] In Example 2.2 we considered a situation where we
are allowed a single action on our state, namely to swap elements. Analogously
to the previous example, we can formalise this in our semantic environment
$S^{\omega}$ by adding to $\Lambda_{S^{\omega}}$ constants
$c_{l,l^{\prime}}:S\to S$ for each pair $l,l^{\prime}\in\\{1,2,3\\}$ along
with the axiom

$[\alpha](\pi)\Rightarrow[\alpha[l\leftrightarrow
l^{\prime}]](c_{l,l^{\prime}}\pi)$

ranging over state formulas $\alpha$ of the form (2) and locations
$l,l^{\prime}\in\\{1,2,3\\}$ of $\mathrm{SL}$, together with axioms
corresponding to those of $\Delta_{H}$ i.e.

$\displaystyle(\pi)\Rightarrow\mathsf{sorted}(\pi)\ \ \ \mbox{and}\ \ \ [l\leq
l^{\prime}\vee l^{\prime}\leq l](\pi)$

Similarly, for each $l,l^{\prime}\in\\{1,2,3\\}$ we add a term
$\mathsf{swap}_{l,l^{\prime}}:C$ to $\Lambda_{S}$ and define
$[\mathsf{swap}_{l,l^{\prime}}]\pi:=\langle{(),c_{l,l^{\prime}}\pi}\rangle$ so
that

${\mathsf{swap}_{l,l^{\prime}}}\;\mathrm{sr}\;{\\{{\alpha}\cdot{\top}\cdot{\alpha[l\leftrightarrow
l^{\prime}]}\\}}$

A derivation of a closed term $t:C$ of
$\mathrm{ST}+\\{\mathsf{swap}_{l,l^{\prime}}\\}$ such that
${[t]}\;\mathrm{sr}\;{\\{{\top}\cdot{\top}\cdot{\mathsf{sorted}}\\}}$ is given
below. In particular, we can prove in $S^{\omega}$ that
$\forall\pi^{S}\,\mathsf{sorted}(\mathsf{proj}_{1}([t]\pi))$, and so the term
$\lambda\pi\,.\,\mathsf{proj}_{1}([t]\pi):S\to S$ acts as a sorting program
for arrays of length three. For an extracted term $t$ corresponding to the
proof given in Example 2.2, first we interpret $\mathcal{D}_{1}$ as

$\vdash\mathsf{skip}:C$ $\;\scriptstyle cons$ $\vdash\mathsf{skip}:C$
$\vdash\mathsf{skip}:C$ $\;\scriptstyle cons$ $\vdash\mathsf{skip}:C$
$\;\scriptstyle 2\leftrightarrow 3$ $\vdash\mathsf{swap}_{2,3}:C$
$\;\scriptstyle cons$ $\vdash\mathsf{swap}_{2,3}:C$ $\;\scriptstyle cond[2\leq
3\vee 3\leq 2]$ $\vdash t_{1}:=\mathsf{if}\,{(2\leq
3)}\,\mathsf{then}\,{(\mathsf{skip})}\,\mathsf{else}\,{(\mathsf{swap}_{2,3})}:C$

and define $t_{1}:=\mathsf{if}\,{(2\leq
3)}\,\mathsf{then}\,{(\mathsf{skip})}\,\mathsf{else}\,{(\mathsf{swap}_{2,3})}$.
Now $\mathcal{D}_{2}$ is interpreted as

$\;\scriptstyle 1\leftrightarrow 2$ $\vdash\mathsf{swap}_{1,2}:C$
$\mathcal{D}_{1}$ $\vdash t_{1}:C$ $\;\scriptstyle\wedge_{S}I$
$\vdash\mathsf{swap}_{1,2}\circ t_{1}:C\times C$
$\;\scriptstyle\wedge_{S}E_{L}$ $\vdash
t_{2}:=\mathsf{swap}_{1,2}\,\ast\,t_{1}:C$

where we define $t_{2}:=\mathsf{swap}_{1,2}\,\ast\,t_{1}:C$. Continuing,
$\mathcal{D}_{3}$ is interpreted as:

$\mathcal{D}_{2}$ $\vdash t_{2}:C$ $\vdash\mathsf{skip}:C$ $\;\scriptstyle
cons$ $\vdash\mathsf{skip}:C$ $\;\scriptstyle cond[2\leq 1\vee 1\leq 2]$
$t_{3}:=\mathsf{if}\,{(2\leq
1)}\,\mathsf{then}\,{t_{2}}\,\mathsf{else}\,{(\mathsf{skip})}:C$

where $t_{3}:=\mathsf{if}\,{(2\leq
1)}\,\mathsf{then}\,{t_{2}}\,\mathsf{else}\,{(\mathsf{skip})}$, and finally

$\vdash\mathsf{skip}:C$ $\;\scriptstyle 2\leftrightarrow 3$
$\vdash\mathsf{swap}_{2,3}:C$ $\;\scriptstyle cond[2\leq 3\vee 3\leq 2]$
$\vdash\mathsf{if}\,{(2\leq
3)}\,\mathsf{then}\,{(\mathsf{skip})}\,\mathsf{else}\,{(\mathsf{swap}_{2,3})}:C$
$\mathcal{D}_{3}$ $\vdash t_{3}:C$ $\;\scriptstyle\wedge_{S}I$
$\vdash(\mathsf{if}\,{(2\leq
3)}\,\mathsf{then}\,{(\mathsf{skip})}\,\mathsf{else}\,{(\mathsf{swap}_{2,3})})\circ
t_{3}:C\times C$ $\;\scriptstyle\wedge_{S}E_{L}$ $\vdash
t:=(\mathsf{if}\,{(2\leq
3)}\,\mathsf{then}\,{(\mathsf{skip})}\,\mathsf{else}\,{(\mathsf{swap}_{2,3})})\,\ast\,t_{3}:C$

##  6\. An extension to arithmetic

We now present an extension of our framework to a stateful version of first-
order intuitionistic arithmetic. On the logic side, we will add not only a
stateful induction rule, but also a Hoare-style while rule for iteration over
the natural numbers. On the computational side, these will be interpreted by
stateful recursion in all finite types, along with a controlled while loop.
The addition of these constants will allow us to extract programs that are
more interesting than those obtainable from proofs in pure predicate logic,
and which can be clearly compared to well-known stateful algorithms. To
exemplify this, we will present a formally synthesised version of insertion
sort, and we stress that by further extending our framework with additional
rules and terms, we would be able to extract an even richer variety of
combined functional/stateful programs.

###  6.1. The system $\mathrm{SA}$: First-order arithmetic with state

Our system of stateful intuitionistic arithmetic $\mathrm{SA}$ builds on
$\mathrm{SL}$ just as ordinary first-order Heyting arithmetic builds on first-
order predicate logic. In both cases, we introduce a constant $0$, a unary
successor symbol $\mathrm{succ}$, symbols for all primitive recursive
functions, and our predicate symbols now include an equality relation $=$. In
what follows we write $x+1$ instead of $\mathrm{succ}(x)$. The axioms and
rules of $\mathrm{SA}$ are, in turn, analogous to the additional axioms and
rules we would require in ordinary first-order arithmetic: They include all
axioms and rules of $\mathrm{SL}$ (based now on the language of
$\mathrm{SA}$), along with a collection of additional axioms and rules. These
comprise not only basic axioms and rules for equality and the successor, and
an induction rule (all now adapted to incorporate the state), but also a new
while rule for stateful iteration, which now exploits our state and, as we
will see, allows us to extract programs that contain while loops. These
additional axioms and rules are given in Figure 4.

Figure 4. Additional axioms and rules of $\mathrm{SA}$
$\begin{gathered}\textbf{Axioms and rules for equality}\\\\[5.69054pt]
\Gamma\vdash_{S}\\{{\alpha}\cdot{t=t}\cdot{\alpha}\\}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{s=t}\cdot{\beta}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to68.1362pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{t=s}\cdot{\beta}\\}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{r=s}\cdot{\beta}\\}\
\ \ \Gamma\vdash_{S}\\{{\beta}\cdot{s=t}\cdot{\gamma}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to151.23094pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
41.7359pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{r=t}\cdot{\gamma}\\}$}\kern
0.0pt$}}\kern 41.7359pt}}}\kern 0.0pt}}}\\\\[5.69054pt] {\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{s=t}\cdot{\beta}\\}\
\ \ \Gamma\vdash_{S}\\{{\beta}\cdot{A(s)}\cdot{\gamma(s)}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to160.85147pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle ext$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
42.2741pt\hbox{\hbox{$\kern
0.0pt\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A(t)}\cdot{\gamma(t)}\\}$}\kern
0.0pt$}}\kern 42.2741pt}}}\kern 12.56557pt}}}\\\\[5.69054pt] \textbf{Axioms
and rules for arithmetical function symbols}\\\\[5.69054pt]
\Gamma\vdash_{S}\\{{\alpha}\cdot{\mathrm{succ}(t)\neq
0}\cdot{\alpha}\\}\qquad{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\\{{\alpha}\cdot{\mathrm{succ}(s)=\mathrm{succ}(t)}\cdot{\beta}\\}$}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to98.7964pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
24.77785pt\hbox{\hbox{$\kern
0.0pt\hbox{$\\{{\alpha}\cdot{s=t}\cdot{\beta}\\}$}\kern 0.0pt$}}\kern
24.77785pt}}}\kern 0.0pt}}}\\\\[5.69054pt]
\Gamma\vdash_{S}\\{{\alpha}\cdot{l=r}\cdot{\alpha}\\}\ \ \ \mbox{where $l=r$
ranges across defining equations for prim. rec. functions}\\\\[5.69054pt]
\textbf{Induction rule}\\\\[5.69054pt] {{}{}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\Gamma\vdash_{S}\\{{\alpha}\cdot{A(0)}\cdot{\beta(0)}\\}$}}\kern
10.00002pt}\hbox{\hbox{$\Gamma,A(x)\vdash_{S}\\{{\beta(x)}\cdot{A(x+1)}\cdot{\beta(x+1)}\\}$}}}}}\kern
1.43518pt\hbox{\kern 0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to242.07355pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle ind$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
55.84001pt\hbox{\hbox{$\Gamma\vdash_{S}\\{{\gamma}\cdot{\forall
x\,\\{{\alpha}\cdot{A(x)}\cdot{\beta(x)}\\}}\cdot{\gamma}\\}$}}\kern
55.84001pt}}}\kern 13.03435pt}}}\\\\[5.69054pt] \textbf{While rule (over
natural numbers)}\\\\[5.69054pt] {{}{}{}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\kern
20.75526pt\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\mathcal{A}_{1}$}}\kern
10.00002pt}\hbox{\hbox{$\mathcal{A}_{2}$}}\kern
10.00002pt}\hbox{\hbox{$\mathcal{A}_{3}$}}}}\kern 20.75526pt}\kern
1.43518pt\hbox{\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to92.41063pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$\;\scriptstyle while$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\Gamma,A(x)\vdash_{S}\\{{\alpha(x)}\cdot{B}\cdot{\beta}\\}$}}}}}\kern
19.90796pt}}}\\\\[5.69054pt]
\mathcal{A}_{1}:=\Gamma,A(x+1)\vdash_{S}\\{{\gamma(x+1)\wedge\alpha(x+1)}\cdot{A(x)}\cdot{\alpha(x)}\\}\\\
\mathcal{A}_{2}:=\Gamma,A(x+1)\vdash_{S}\\{{\neg\gamma(x+1)\wedge\alpha(x+1)}\cdot{B}\cdot{\beta}\\}\\\
\mathcal{A}_{3}:=\Gamma,A(0)\vdash_{S}\\{{\alpha(0)}\cdot{B}\cdot{\beta}\\}\\\\[5.69054pt]
\mbox{for $ind$ and $while$, $x$ is not free in $\Gamma$, and for $while$ it
is not free in $B$ or $\beta$}\end{gathered}$

Our formulation of stateful arithmetic follows the same basic idea as the
construction of stateful predicate logic, incorporating standard rules but
keeping track of an ambient state in a call-by-value manner, and adding new
rules that explicitly correspond to stateful constructions. In particular,
Proposition 1 clearly extends to $\mathrm{SA}$, as the usual axioms and rules
of arithmetic can be embedded into those of $\mathrm{SA}$:

######  Proposition 11.

For any formula $A$ of $\mathrm{HA}$ and state formula $\alpha$, define the
main formula $A_{\alpha}$ of $\mathrm{SA}$ as in Proposition 1. Then whenever
$\Gamma\vdash_{I}A$ is provable in $\mathrm{HA}$, we have that
$\Gamma_{\alpha},\Delta\vdash_{S}\\{{\alpha}\cdot{A_{\alpha}}\cdot{\alpha}\\}$
is provable in $\mathrm{SA}$, where $\Delta$ is arbitrary and
$\Gamma_{\alpha}:=(A_{1})^{u_{1}}_{\alpha},\ldots,(A_{n})^{u_{n}}_{\alpha}$
for $\Gamma:=A_{1}^{u_{1}},\ldots,A_{n}^{u_{n}}$.

We can also derive a natural extensionality rule from our stateful equality
rules, which assures us that whenever $s=t$ in ordinary Heyting arithmetic,
then we can replace $s$ by $t$ for stateful formulas:

######  Proposition 12.

Suppose that $\vdash_{I}s=t$ is provable in $\mathrm{HA}$. Then from
$\Gamma\vdash_{S}\\{{\alpha(s)}\cdot{A(s)}\cdot{\beta(s)}\\}$ we can derive
$\Gamma\vdash_{S}\\{{\alpha(t)}\cdot{A(t)}\cdot{\beta(t)}\\}$ in
$\mathrm{SA}$.

######  Proof 6.1.

By Proposition 11 for $\alpha:=\alpha(s)$ we have
$\Gamma\vdash_{S}\\{{\alpha(s)}\cdot{s=t}\cdot{\alpha(s)}\\}$ and thus using
the extensionality rule in $\mathrm{SA}$ we can derive

$\Gamma\vdash_{S}\\{{\alpha(s)}\cdot{s=t}\cdot{\alpha(s)}\\}\ \ \
\Gamma\vdash_{S}\\{{\alpha(s)}\cdot{A(s)}\cdot{\beta(s)}\\}$ $\;\scriptstyle
ext$ $\Gamma\vdash_{S}\\{{\alpha(s)}\cdot{A(t)}\cdot{\beta(t)}\\}$

Since $\vdash_{I}t=s$ must also be provable in $\mathrm{HA}$, another instance
of Proposition 11 for $\alpha:=\alpha(t)$ along with the true axiom in
$\mathrm{SA}$ gives us

$\Gamma\vdash_{S}\\{{\alpha(t)}\cdot{t=s}\cdot{\alpha(t)}\\}\ \ \
\Gamma\vdash_{S}\\{{\alpha(t)}\cdot{\top}\cdot{\alpha(t)}\\}$ $\;\scriptstyle
ext$ $\Gamma\vdash_{S}\\{{\alpha(t)}\cdot{\top}\cdot{\alpha(s)}\\}$

Putting these together we obtain

$\Gamma\vdash_{S}\\{{\alpha(t)}\cdot{\top}\cdot{\alpha(s)}\\}$$\Gamma\vdash_{S}\\{{\alpha(s)}\cdot{A(t)}\cdot{\beta(t)}\\}$
$\;\scriptstyle\wedge_{S}I$ $\Gamma\vdash_{S}\\{{\alpha(t)}\cdot{\top\wedge
A(t)}\cdot{\beta(t)}\\}$ $\;\scriptstyle\wedge_{S}E_{L}$
$\Gamma\vdash_{S}\\{{\alpha(t)}\cdot{A(t)}\cdot{\beta(t)}\\}$

which completes the derivation.

###  6.2. An extended term calculus $\mathrm{ST}_{N}$

In order to give derivations in $\mathrm{SA}$ a computation interpretation, we
need to extend our term calculus $\mathrm{ST}$ to include a recursor (for
induction) and a controlled while loop (for the while rule). The remaining new
axioms and rules of $\mathrm{SA}$ are dealt with in a straightforward manner.

To be precise: the theory $\mathrm{ST}_{N}$ is defined to be the instance of
$\mathrm{ST}$ for the case of arithmetic, with function symbols for zero,
successor and all primitive recursive functions. Accordingly, we rename the
base type $D$ to ${\rm Nature}$. In addition to the terms of $\mathrm{ST}$, we
add terms $\mathsf{rec}\,{e}\,{e}$ and
$\mathsf{while}_{e}\,{\gamma[z]}\,{e}\,{e}\,{e}$ to our grammar, where
$\gamma[z]$ ranges over state formulas of $\mathrm{SL}$ with a specified free
variable $z$. The typing rules for these new terms are

$\frac{\Gamma\vdash s:X\ \ \ \Gamma\vdash t:{\rm Nature}\to X\to
X}{\Gamma\vdash\mathsf{rec}\,{s}\,{t}:{\rm Nature}\to X}$

for the recursor, while for the while loop we have

$\frac{\Gamma\vdash r:{\rm Nature}\to X\to X\ \ \ \Gamma\vdash s:{\rm
Nature}\to X\to Y\ \ \ \Gamma\vdash t:X\to Y\ \ \ \Gamma\vdash u:{\rm
Nature}}{\Gamma\vdash\mathsf{while}_{u}\,{\gamma[z]}\,{r}\,{s}\,{t}:X\to Y}$

under the additional variable condition that $z\notin\Gamma$, but $x:{\rm
Nature}\in\Gamma$ for all free variables of $\gamma[z]$ outside of $z$. Note
that we do not consider $z$ a free variable of
$\mathsf{while}_{a}\,{\gamma[z]}\,{r}\,{s}\,{t}$, but rather a placeholder for
the loop condition. In order to give the appropriate semantics to our terms,
we must add to our metatheory $S^{\omega}$ axioms and rules for arithmetic in
all finite types, including the ability to define functions of arbitrary type
via recursion over the natural numbers, along the lines of
$\mathrm{E}\mbox{-}\mathrm{HA}^{\omega}$ [Tro73] (though as before the precise
details are not important). We then define:

  * •

$[\mathsf{rec}\,{s}\,{t}]\pi:=\langle{R_{f},\pi_{1}}\rangle$ for
$\langle{f,\pi_{1}}\rangle:=[t]\pi$, where

$\displaystyle R_{f}0\pi$ $\displaystyle:=[s]\pi$ (3) $\displaystyle
R_{f}(n+1)\pi$ $\displaystyle:=ga\pi^{\prime}_{2}\mbox{ for
$\langle{a,\pi^{\prime}_{1}}\rangle:=R_{f}n\pi^{\prime}$ and
$\langle{g,\pi^{\prime}_{2}}\rangle:=fn\pi^{\prime}_{1}$}$

  * •

$[\mathsf{while}_{u}\,{\gamma[z]}\,{r}\,{s}\,{t}]\pi:=\langle{L_{f,g,h}m,\pi_{4}}\rangle$
where $\langle{f,\pi_{1}}\rangle:=[r]\pi$,
$\langle{g,\pi_{2}}\rangle:=[s]\pi_{1}$,
$\langle{h,\pi_{3}}\rangle:=[t]\pi_{2}$ and
$\langle{m,\pi_{4}}\rangle:=[u]\pi_{3}$, where

$\displaystyle L_{f,g,h}0y\pi^{\prime}:=hy\pi^{\prime}$ (4) $\displaystyle
L_{f,g,h}(n+1)y\pi^{\prime}$
$\displaystyle:=\begin{cases}L_{f,g,h}ny^{\prime}\pi_{2}\mbox{ for
$\langle{a,\pi^{\prime}_{1}}\rangle:=fn\pi^{\prime}$ and
$\langle{y^{\prime},\pi^{\prime}_{2}}\rangle:=ay\pi^{\prime}_{1}$}&\mbox{if
$[\gamma][n+1](\pi^{\prime})$}\\\ by\pi^{\prime}_{1}\mbox{ for
$\langle{b,\pi^{\prime}_{1}}\rangle:=gn\pi^{\prime}$}&\mbox{if
$\neg[\gamma][n+1](\pi^{\prime})$}\end{cases}$

where in the case distinctions, we would technically speaking need to use the
characteristic function
$\chi_{\gamma}\langle{x_{1},\ldots,n,\ldots,x_{k}}\rangle$ for $\gamma$, with
$n$ substituted for the special free variable $z$.

###  6.3. The soundness theorem for arithmetic

We now need to show that the soundness proof for stateful predicate logic also
holds in the extension to arithmetic.

######  Theorem 13.

The statement of Theorem 9 remains valid if we replace $\mathrm{SL}$ by
$\mathrm{SA}$ and $\mathrm{ST}$ by $\mathrm{ST}_{N}$.

######  Proof 6.2.

We need to extend the proof of Theorem 13 to show that the additional axioms
and rules as in Figure 4 can be realized by a term of the form $[t]$ for $t$
in $\mathrm{ST}_{N}$.

  * •

For the non-extensionality equality and arithmetic axioms this is
straightforward due to the fact that these are also true in $S^{\omega}$: For
instance, given a realizer
${[s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{u=v}\cdot{\beta}\\}}$ and
${[t]}\;\mathrm{sr}\;{\\{{\beta}\cdot{v=w}\cdot{\gamma}\\}}$, we have that
${[s\circ t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{u=v\wedge
v=w}\cdot{\gamma}\\}}$, and since from $u=v\wedge v=w$ we can infer $u=w$ in
$S^{\omega}$, it follows that ${[p_{1}(s\circ
t)]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{u=w}\cdot{\gamma}\\}}$. The other axioms
and rules are even simpler.

  * •

$(ext)$ Extensionality is similarly simple: If
${[s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{u=v}\cdot{\beta}\\}}$ and
${[t]}\;\mathrm{sr}\;{\\{{\beta}\cdot{A(u)}\cdot{\gamma(u)}\\}}$, then
$[\alpha](\pi)$ implies that $u=v$ and $[\beta](\pi_{1})$ for
$\langle{\ldots,\pi_{1}}\rangle:=[s]\pi$, and therefore
${a}\;\mathrm{sr}\;{A(u)}$ and $[\gamma](u)(\pi_{2})$ for
$\langle{a,\pi_{2}}\rangle:=[t]\pi_{1}$. Now applying extensionality in
$S^{\omega}$ to the formula
$T(x):={a}\;\mathrm{sr}\;{A(x)}\wedge[\gamma](x)(\pi_{2})$, from $u=v$ we have
${a}\;\mathrm{sr}\;{A(v)}$ and $[\gamma](v)(\pi_{2})$, and thus ${[s\circ
t]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{u=v\wedge A(v)}\cdot{\gamma(v)}\\}}$ and
therefore ${[p_{2}(s\circ
t)]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A(v)}\cdot{\gamma(v)}\\}}$.

  * •

$(rec)$ Suppose that $s$ and $t(x,y)$ are such that
${[s]}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A(0)}\cdot{\beta(0)}\\}}$ and

${[t](x,y)}\;\mathrm{sr}\;{\\{{\beta(x)}\cdot{A(x+1)}\cdot{\beta(x+1)}\\}}$

assuming ${y}\;\mathrm{sr}\;{A(x)}$. We show that
${[\mathsf{rec}\,{s}\,{\lambda
x,y.t(x,y)}]}\;\mathrm{sr}\;{\\{{\gamma}\cdot{\forall
x\,\\{{\alpha}\cdot{A(x)}\cdot{\beta(x)}\\}}\cdot{\gamma}\\}}$ for any
$\gamma$. Since $[\mathsf{rec}\,{s}\,{\lambda
x,y.t(x,y)}]\pi=\langle{R_{f},\pi}\rangle$ for $f:=\lambda x.[\lambda
y.t(x,y)]$ and $R_{f}$ as in (3), it suffices to show that for any $n:{\rm
Nature}$ we have

${R_{f}n}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A(n)}\cdot{\beta(n)}\\}}$

We prove this by induction: For the base case, we have $R_{f}0=[s]$ and the
claim holds by assumption. For the induction step, let us assume that
$[\alpha](\pi^{\prime})$ holds, and so by the induction hypothesis we have
${a}\;\mathrm{sr}\;{A(n)}$ and $[\beta(n)](\pi^{\prime}_{1})$ for
$\langle{a,\pi^{\prime}_{1}}\rangle:=R_{f}n$. Since
$fn\pi^{\prime}_{1}=\langle{g,\pi^{\prime}_{1}}\rangle$ for $g:=\lambda
y.[t](n,y)$, we have that $R_{f}(n+1)\pi^{\prime}=[t](n,a)\pi^{\prime}_{1}$,
and since by the property of $[t]$ we then have ${b}\;\mathrm{sr}\;{A(n+1)}$
and $[\beta(n+1)](\pi^{\prime}_{2})$ for
$\langle{b,\pi^{\prime}_{2}}\rangle:=[t](n,a)\pi^{\prime}_{1}$, we have shown
that
${R_{f}(n+1)}\;\mathrm{sr}\;{\\{{\alpha}\cdot{A(n+1)}\cdot{\beta(n+1)}\\}}$,
which completes the induction.

  * •

$(while)$ We suppose that

    1. (1)

${[r](x,y)}\;\mathrm{sr}\;{\\{{\gamma(x+1)\wedge\alpha(x+1)}\cdot{A(x)}\cdot{\alpha(x)}\\}}$
assuming that ${y}\;\mathrm{sr}\;{A(x+1)}$,

    2. (2)

${[s](x,y)}\;\mathrm{sr}\;{\\{{\neg\gamma(x+1)\wedge\alpha(x+1)}\cdot{B}\cdot{\beta}\\}}$
assuming that ${y}\;\mathrm{sr}\;{A(x+1)}$,

    3. (3)

${[t](y)}\;\mathrm{sr}\;{\\{{\alpha(0)}\cdot{B}\cdot{\beta}\\}}$ assuming that
${y}\;\mathrm{sr}\;{A(0)}$.

Our aim is to show that

${[(\mathsf{while}_{x}\,{\gamma}\,{(\lambda
x^{\prime},y^{\prime}.r)}\,{(\lambda x^{\prime},y^{\prime}.s)}\,{(\lambda
y^{\prime}.t)})y]}\;\mathrm{sr}\;{\\{{\alpha(x)}\cdot{B}\cdot{\beta}\\}}$

for any $x,y\in{\rm Nature}$ with ${y}\;\mathrm{sr}\;{A(x)}$. We observe,
unwinding the definition, that

$[(\mathsf{while}_{x}\,{\gamma}\,{(\lambda
x^{\prime},y^{\prime}.r)}\,{(\lambda x^{\prime},y^{\prime}.s)}\,{(\lambda
y^{\prime}.t)})y]\pi=L_{f,g,h}xy\pi$

for $f:=\lambda x^{\prime}.[\lambda y^{\prime}.r(x^{\prime},y^{\prime})]$,
$g:=\lambda x^{\prime}.[\lambda y^{\prime}.s(x^{\prime},y^{\prime})]$,
$h:=\lambda y^{\prime}.[t](y^{\prime})$ and $L_{f,g,h}$ as defined in (4). We
now show by induction on $n$ that if ${y}\;\mathrm{sr}\;{A(n)}$ then

${L_{f,g,h}ny}\;\mathrm{sr}\;{\\{{\alpha(n)}\cdot{B}\cdot{\beta}\\}}$

and then the result follows by setting $n:=x$. The base case is
straightforward since

$L_{f,g,y}0y=[t](y)$

and the claim follows by definition of $[t]$. For the induction step, suppose
that ${y}\;\mathrm{sr}\;{A(n+1)}$ and $[\alpha(n+1)](\pi)$. There are two
cases. If $\neg[\gamma](n+1)(\pi)$ we have

$L_{f,g,h}(n+1)y\pi=[s](n,y)\pi$

and the result holds by the property of $[s]$. On the other hand, if
$[\gamma](n+1)(\pi)$ then

$L_{f,g,h}(n+1)y\pi=L_{f,g,h}ny^{\prime}\pi^{\prime}$

for $\langle{y^{\prime},\pi^{\prime}}\rangle:=[r](n,y)\pi$. But by the
property of $[r]$ we have ${y^{\prime}}\;\mathrm{sr}\;{A(n)}$ and
$[\alpha(n)](\pi^{\prime})$, and therefore by the induction hypothesis we have
${b}\;\mathrm{sr}\;{B}$ and $[\beta](\pi^{\prime\prime})$ for
$\langle{b,\pi^{\prime\prime}}\rangle:=L_{f,g,h}ny^{\prime}\pi^{\prime}=L_{f,g,h}(n+1)y\pi$,
and so the result is proven for $n+1$.

This covers all the additional axioms and rules of $\mathrm{SA}$.

###  6.4. Worked example: Insertion sort

We now illustrate our extended system by synthesising a list sorting program
that, intuitively, forms an implementation of the insertion sort algorithm.
Here our state will represent the structure that is to be sorted, and
continuing the spirit of generality that we have adhered to throughout, we
characterise this structure through a number of abstract axioms. Instantiating
the state as, say, an array of natural numbers, would provide a model for our
theory, but our sorting algorithm can be extracted on the more abstract level.
Crucially, the proof involves both loop iteration and induction, and the
corresponding program combines an imperative while loop with a functional
recursor.

We begin by axiomatising our state, just as in previous examples. An intuition
here is that states represent an infinite array of elements
$a_{0},a_{1},\ldots$ possessing some total order structure $\leq$, and we seek
to extract a program that, for any input $n$, sorts the first $n$ elements. We
use this informal semantics throughout to indicate the intended meaning of our
axioms, but stress that none of this plays a formal role in the proof or
resulting computational interpretation.

We introduce three state predicates to $\mathrm{SA}$, with the intuition
indicated in each case:

  * •

$\mathsf{sort}(N)$ – _Sorted: The first $N+1$ elements of the array i.e.
$[a_{0},\ldots,a_{N}]$ are sorted_

  * •

$\mathsf{psort}(n,N)$ – _Partially sorted with respect to $a_{n}$: if $n<N$
then the list_

$[a_{0},\ldots,a_{n-1},a_{n+1},\ldots,a_{N}]$

_is sorted and $a_{n}\leq a_{n+1}$. For the base cases, if $n=N$ then the list
$[a_{0},\ldots,a_{N-1}]$ is sorted, and if $n>N$ then the list
$[a_{0},\ldots,a_{N}]$ is sorted._

  * •

$\mathsf{comp}(n)$ – _Comparison: true if $a_{n}\leq a_{n-1}$, and always true
if $n=0$_

We formalise this intuition by adding the following state independent axioms
to $\Delta_{H}$:

  1. (1)

$\Gamma,\mathsf{sort}(N)\vdash_{H}\mathsf{psort}(N+1,N+1)$ – _If the first
$N+1$ elements are sorted, then they are also partially sorted with respect to
the next element $a_{N+1}$._

  2. (2)

$\Gamma,\neg\mathsf{comp}(n),\mathsf{psort}(n,N)\vdash_{H}\mathsf{sort}(N)$ –
_If $[a_{0},\ldots,a_{n-1},a_{n+1},\ldots,a_{N}]$ is sorted, $a_{n}\leq
a_{n+1}$, but also $a_{n-1}\leq a_{n}$, then the entire segment
$[a_{0},\ldots,a_{N}]$ must be sorted._

  3. (3)

$\Gamma,\mathsf{psort}(0,N)\vdash_{H}\mathsf{sort}(N)$ – _If
$[a_{1},\ldots,a_{N}]$ is sorted and $a_{0}\leq a_{1}$, then
$[a_{0},\ldots,a_{N}]$ is sorted._

  4. (4)

$\Gamma\vdash_{H}\mathsf{sort}(0)$ – _The singleton array $[a_{0}]$ is defined
to be sorted._

We complete the axiomatisation by adding a single state-sensitive axiom to
$\Delta_{S}$:

  1. (5)

$\Gamma\vdash_{S}\\{{\mathsf{comp}(n+1)\wedge\mathsf{psort}(n+1,N)}\cdot{\top}\cdot{\mathsf{psort}(n,N)}\\}$
– _If $[a_{0},\ldots,a_{n},a_{n+2},\ldots,a_{N}]$ is sorted and $a_{n+1}\leq
a_{n+2}$, but $a_{n+1}\leq a_{n}$, then we can modify the state (i.e. swapping
$a_{n}$ and $a_{n+1}$ by setting $\tilde{a}_{n}:=a_{n+1}$ and
$\tilde{a}_{n+1}:=a_{n}$) so that
$[a_{0},\ldots,a_{n-1},\tilde{a}_{n+1},\ldots,a_{N}]$ is sorted and
$\tilde{a}_{n}\leq\tilde{a}_{n+1}$. The edge cases for $n\geq N$ are
interpreted in a more straightforward way._

In order to give a realizing term to this axiom, we representing element
swapping semantically by adding a constant $c:{\rm Nature}\to S\to S$ to our
metatheory $S^{\omega}$, which satisfies

$\mathsf{comp}(n+1,\pi)\wedge\mathsf{psort}(n+1,N,\pi)\Rightarrow\mathsf{psort}(n,N,cn\pi)$

and a corresponding term $\mathsf{swap}:{\rm Nature}\to C$ to our term
calculus, along with the embedding

$[\mathsf{swap}]\pi:=\langle{\lambda
n,\pi.\langle{(),cn\pi}\rangle,\pi}\rangle\simeq\langle{c,\pi}\rangle$

so that we can prove

${[\mathsf{swap}\,n]}\;\mathrm{sr}\;{\\{{\mathsf{comp}(n+1)\wedge\mathsf{psort}(n+1,N)}\cdot{\top}\cdot{\mathsf{psort}(n,N)}\\}}$

With this in place, we can now prove in $\mathrm{SA}$ that the first $N$
elements of the state can be sorted, and extract a corresponding realizing
term in $\mathrm{ST}_{N}$.

####  6.4.1. Proof of $\vdash_{S}\\{{\gamma}\cdot{\forall
N\,\\{{\alpha}\cdot{\top}\cdot{\mathsf{sort}(N)}\\}}\cdot{\gamma}\\}$ in
$\mathrm{SA}$

The core of our proof begins with an instance of the $while$ rule parametrised
by $N$, with $\Gamma:=\emptyset$, $A(n):=\top$,
$\alpha(n):=\mathsf{psort}(n,N+1)$, $\beta:=\mathsf{sort}(N+1)$ and
$\gamma(n):=\mathsf{comp}(n)$:

$\mathcal{D}_{1}\ \ \ \mathcal{D}_{2}\ \ \ \mathcal{D}_{3}$ $\;\scriptstyle
while$
$\top\vdash_{S}\\{{\mathsf{psort}(n,N+1)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$
$\;\scriptstyle\forall_{S}I$
$\top\vdash_{S}\\{{\mathsf{psort}(N+1,N+1)}\cdot{\forall
n\,\\{{\mathsf{psort}(n,N+1)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}}\cdot{\mathsf{psort}(N+1,N+1)}\\}$
$\;\scriptstyle\forall_{S}E$
$\top\vdash_{S}\\{{\mathsf{psort}(N+1,N+1)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$
$\;\scriptstyle cons$
$\top\vdash_{S}\\{{\mathsf{sort}(N)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$

where the final composition inference makes use of the first state independent
axiom. Here $\mathcal{D}_{1}$ represents an instance of the state sensitive
axiom

$\top\vdash_{S}\\{{\mathsf{comp}(n+1)\wedge\mathsf{psort}(n+1,N+1)}\cdot{\top}\cdot{\mathsf{psort}(n,N+1)}\\}$

and $\mathcal{D}_{2}$ represents the derivation

$\top\vdash_{S}\\{{\mathsf{sort}(N+1)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$
$\;\scriptstyle cons$
$\top\vdash_{S}\\{{\neg\mathsf{comp}(n+1)\wedge\mathsf{psort}(n+1,N+1)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$

where composition makes use of the second state independent axiom. Finally
$\mathcal{D}_{3}$ is

$\top\vdash_{S}\\{{\mathsf{sort}(N+1)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$
$\;\scriptstyle cons$
$\top\vdash_{S}\\{{\mathsf{psort}(0,N+1)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$

this time making use of the third state independent axiom. Finally we can
prove that all lists can be sorted with an outer induction as follows:

$\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\alpha}\\}$ $\;\scriptstyle cons$
$\vdash_{S}\\{{\alpha}\cdot{\top}\cdot{\mathsf{sort}(0)}\\}$ $\mathcal{D}$
$\top\vdash_{S}\\{{\mathsf{sort}(N)}\cdot{\top}\cdot{\mathsf{sort}(N+1)}\\}$
$\;\scriptstyle ind$ $\vdash_{S}\\{{\gamma}\cdot{\forall
N\,\\{{\alpha}\cdot{\top}\cdot{\mathsf{sort}(N)}\\}}\cdot{\gamma}\\}$

where $\alpha$ is an arbitrary state predicate, the instance of $cons$ uses
the fourth state independent axiom, and $\mathcal{D}$ represents the
derivation above.

####  6.4.2. Program extraction

We now extract a program that corresponds to the above proof. First of all, we
note that the three premises of our while rule are realised by
$\mathsf{swap}\,n$, $\mathsf{skip}$ and $\mathsf{skip}$ respectively, and so
our derivation $\mathcal{D}$ corresponds to the following program:

$y:C\vdash\mathsf{swap}\,n:C\ \ \ y:C\vdash\mathsf{skip}:C\ \ \
y:C\vdash\mathsf{skip}:C$ $\;\scriptstyle while$ $y:C\vdash t(n)y:C$
$\;\scriptstyle\forall_{S}I$ $y:C\vdash\lambda n.t(n)y:{\rm Nature}\to C$
$\;\scriptstyle\forall_{S}E$ $y:C\vdash(\lambda n.t(n)y)(N+1):C$
$\;\scriptstyle cons$ $y:C\vdash(\lambda n.t(n)y)(N+1):C$

where

$\displaystyle t(n)$
$\displaystyle:=\mathsf{while}_{n}\,{\mathsf{comp}[z]}\,{(\lambda
x,y.(\mathsf{swap}\,x))}\,{(\lambda x,y.\mathsf{skip})}\,{(\lambda
y.\mathsf{skip})}$
$\displaystyle\simeq\mathsf{while}_{n}\,{\mathsf{comp}[z]}\,{(\lambda
x.(\mathsf{swap}\,x))}\,{(\mathsf{skip})}\,{(\mathsf{skip})}$

Then our final induction generates the following program:

$\vdash\mathsf{skip}:C$$y:C\vdash(\lambda n.t(n)y)(N+1):C$ $\;\scriptstyle
ind$ $\vdash\mathsf{rec}\,{(\mathsf{skip})}\,{(\lambda x,y.((\lambda
n.t(n)y)(x+1)))}:{\rm Nature}\to C$

Thus our list sorting program is

$\displaystyle\mathsf{rec}\,{(\mathsf{skip})}\,{(\lambda x,y.((\lambda
n.t(n)y)(x+1)))}$
$\displaystyle\simeq\mathsf{rec}\,{(\mathsf{skip})}\,{(\lambda x.((\lambda
n.(\mathsf{while}_{n}\,{\mathsf{comp}[z]}\,{(\lambda
x.(\mathsf{swap}\,x))}\,{(\mathsf{skip})}\,{(\mathsf{skip})}()))(x+1)))}$

which is essentially an implementation of the insertion sort algorithm, with
an outer recursion that sorts initial segments of the list in turn, and an
inner loop that inserts new elements into the appropriate place in the current
sorted list.

##  7\. Directions for future work

In this paper we have presented the central ideas behind a new method for
extracting stateful programs from proofs, which include an extension of
ordinary first-order logic with Hoare triples, a corresponding realizability
interpretation, and a soundness theorem. We emphasise once again that our
intention has been to offer an alternative approach to connecting proofs with
stateful programs, one that seeks to complement rather than improve existing
work by embracing simplicity and abstraction, and which might be well suited
to a range of applications in proof theory or computability theory. In this
spirit, we conclude with a very informal outline of a series interesting
directions in which we anticipate that our framework could be applied.

###  7.1. Further extensions and program synthesis

While our main results have been presented in the neutral setting of first-
order predicate logic, it would be straightforward to extend $\mathrm{SL}$ to
richer logics with more complex data structures and imperative commands.
Already, the addition of recursion and loops over natural numbers in Section 6
has allowed us to synthesise a standard in-place sorting algorithm using our
abstract axiomatisation of an ordered state, in a similar spirit to [BSW14].
However, further extensions are naturally possible, including the addition of
general fixpoint operators and non-controlled while loops, which would then
require a $S^{\omega}$ to be replaced by a domain theoretic semantics that
allows for partiality.

Looking a step further ahead, by implementing all of this in a proof
assistant, we would have at our disposal a new technique for synthesising
correct-by-construction imperative programs. While we do not suggest that this
pipeline would directly compete with existing techniques for verifying
imperative programs, it could be well suited to synthesising and reasoning
about programs in very specific domains, where we are interested in algorithms
for which interactions with the state have a restricted form that could be
suitably axiomatised within our logic. For example, a more detailed
axiomatisation our state as an ordered array along the lines of Section 6.4,
with a “swap” operation and a few other ways of interacting with the state,
might give rise to an interesting theory of in-place sort algorithms. Stateful
algorithms on other data structures, such as graphs, could presumably also be
formalised within our framework.

###  7.2. Bar recursion and the semantics of extracted programs

Two of the main starting points for this paper, the monadic realizability of
Birolo [Bir12] and the author’s own Dialectica interpretation with state
[Pow18], address the broader problem of trying to understand the operational
semantics of programs extracted from proofs as stateful procedures (the
origins and development of this general idea, from Hilbert’s epsilon calculus
onwards, is brilliantly elucidated in Chapter 1 of Aschieri’s thesis [Asc11],
who then sets out his own realizability interpretation based on learning). A
number of case studies by the author and others [OP15a, OP15b, Pow20, PSW22]
have demonstrated that while terms extracted from nontrivial proofs can be
extremely complex, they are often much easier to understand if one focuses on
the way they interact with the mathematical environment. For example, in
understanding a program extracted from a proof using Ramsey’s theorem for
pairs [OP15a], it could be illuminating to study the _trace_ of the program as
it queries a colouring at particular pairs, as this can lead to a simpler
characterisation of the _algorithm_ ultimately being implemented by the term.

While the aforementioned analysis of programs has always been done in an
informal way, our stateful realizability interpretation would in theory allow
us to extract programs which store this trace formally in the state, where our
abstract characterisation of state would allow us to implement it in whichever
way is helpful in a given setting. For example, in the case of the Bolzano-
Weierstrass theorem [OP15b], our state might record information of the form
$x_{n}\in I$, collecting information about the location of sequence elements.
For applications in algebra [PSW22], one might instead store information about
a particular maximal ideal.

The aforementioned theorems are typically proven using some form of choice or
comprehension, and that in itself leads to the interesting prospect of
introducing both stateful recursors and while-loops that are computationally
equivalent to variants of _bar recursion_ [Spe62]. In [Pow16], several bar
recursive programs that arise from giving a computational interpretation to
arithmetical comprehension principles are formulated as simple while loops,
and these could in principle be incorporated into our system with new
controlled Hoare rules in the style of update recursion [Ber04], that replace
the conditions $n<N$ and $n\geq N$ in the $\mathcal{A}_{i}$ above with e.g.
$n\in\mathrm{dom}(f)$ and $n\notin\mathrm{dom}(f)$, where $f$ is some partial
approximation to a comprehension function. An exploration of such while-loops
from the perspective of higher-order computability theory might well be of
interest in its own right.

###  7.3. A logic for probabilistic lambda calculi

Probabilistic functional languages are a major topic of research at present.
While work in this direction dates back to the late 1970s [JP89, SD78] where
it typically had a semantic flavour, a more recent theme [DLZ12, DP95, DPHW05]
has been to study simple extensions of the lambda calculus with
nondeterministic choice operators $\oplus$, where $s\oplus t$ evaluates
nondeterministically (or probabilistically) to either $s$ or $t$. While such
calculi have been extensively studied, corresponding _logics_ that map under
some proof interpretation to probabilistic programs are far more rare
(although there is some recent work in this direction e.g. [ADLP22]).

We conjecture that our framework offers a bridge between logic and
probabilistic computation through incorporating probabilistic disjunctions
into our logic $\mathrm{SL}$ and taking states to be streams of outcomes of
probabilistic events together with a current ‘counter’ that increases each
time an event occurs. In a simple setting where only two outcomes are possible
with equal probability, we can axiomatise this within $\mathrm{SL}$ by adding
zero and successor functions (allowing us to create numerals $n$), along with
a unary state predicate $\mathsf{count}(n)$. We can then model probabilistic
events by adding the appropriate axioms to $\Delta_{S}$. Suppose, for example,
we add two predicate constants $H(x)$ and $T(x)$ (for _heads_ and _tails_),
along with constants $c_{1},c_{2},\ldots$ representing coins. Then flipping a
coin would be represented by the axiom schema

$\Gamma\vdash_{S}\\{{\mathsf{count}(n)}\cdot{H(c_{i})\vee
T(c_{i})}\cdot{\mathsf{count}(n+1)}\\}$

where $n$ ranges over numerals and $c_{i}$ over coin constants, the counter
indicating that a probabilistic event has occurred. The act of reading a
probability from the state could be interpreted semantically by introducing a
constant $\omega:S\to\mathrm{Bool}\times S$ to $S^{\omega}$, with the axiom

$\mathsf{count}(n,\pi)\Rightarrow(e=\mathsf{f}\Rightarrow
H(c_{i}))\wedge(e=\mathsf{t}\Rightarrow
T(c_{i}))\wedge\mathsf{count}(n+1,\pi_{1})\mbox{ for
$\langle{e,\pi_{1}}\rangle:=\omega\pi$}$

(alternatively, we could simply define $S:={\rm Nature}\times({\rm
Nature}\to\mathrm{Bool})$ for a type of ${\rm Nature}$ natural numbers, and
define $\omega\langle{n,a}\rangle:=\langle{a(n),\langle{n+1,a}\rangle}\rangle$
and $\mathsf{count}(n,\langle{m,a}\rangle):=m=_{\rm Nature}n$).

A probabilistic choice operator $\oplus$ can then be added to the language of
$\mathrm{ST}$, along with the typing rule $\Gamma\vdash s\oplus t:X+Y$ for
$\Gamma\vdash s:X$ and $\Gamma\vdash t:Y$, and the interpretation

$[s\oplus
t]\pi:=\mathsf{case}\,{e}\,{([\iota_{0}s]\pi_{1})}\,{([\iota_{1}t]\pi_{1})}\mbox{
where $\langle{e,\pi_{1}}\rangle:=\omega\pi$}$

In particular, defining $\mathsf{flip}:=\mathsf{skip}\oplus\mathsf{skip}:C+C$
we would have

${[\mathsf{flip}]}\;\mathrm{sr}\;{\\{{\mathsf{count}(n)}\cdot{H(c_{i})\vee
T(c_{i})}\cdot{\mathsf{count}(n+1)}\\}}$

although we stress that the operator $\oplus$ and would allow for much more
complex probabilistic disjunctions, potentially involving additional
computational content.

Our soundness theorem, extended to these new probabilistic axioms and terms,
would then facilitate the extraction of probabilistic programs from proofs.
For instance, including a winner predicate $W(x)$, two player constant symbols
$p_{1},p_{2}$, and adding axioms

$\displaystyle H(c_{1}),H(c_{2})$
$\displaystyle\vdash_{S}\\{{\alpha}\cdot{W(p_{1})}\cdot{\alpha}\\}$
$\displaystyle T(c_{1}),T(c_{2})$
$\displaystyle\vdash_{S}\\{{\alpha}\cdot{W(p_{1})}\cdot{\alpha}\\}$
$\displaystyle H(c_{1}),T(c_{2})$
$\displaystyle\vdash_{S}\\{{\alpha}\cdot{W(p_{2})}\cdot{\alpha}\\}$
$\displaystyle T(c_{1}),H(c_{2})$
$\displaystyle\vdash_{S}\\{{\alpha}\cdot{W(p_{2})}\cdot{\alpha}\\}$

for any $\alpha$, we could prove

$\vdash_{S}\\{{\mathsf{count}(n)}\cdot{\exists
x\,W(x)}\cdot{\mathsf{count}(n+2)}\\}$

expressing the fact that a winner can be determined after two flips. We can
then extract a corresponding probabilistic term for realizing this statement,
which would be isomorphic to the expected program that queries the state twice
in order to determine the outcome of those flips, and returns either $p_{1}$
or $p_{2}$ as a realizer for $\exists x\,W(x)$ depending on the content of the
state.

Of course, the details here need to be worked through carefully in order to
properly substantiate the claim that our framework could be used to extract
probabilistic programs in a natural and meaningful way. At the very least, it
is likely that further additions to $\mathrm{SL}$ along with a more intricate
state would be needed to incorporate more interesting probabilistic events,
such as annotated disjunctions along the lines of [VVB04]. We leave such
matters to future work.

## Acknowledgments

The author thanks the anonymous referees who provided comments on earlier
versions of this paper, which resulted in a much improved final version.

## References

  * [ADLP22] Melissa Antonelli, Ugo Dal Lago, and Paolo Pistone.  Curry and Howard meet Borel.  In Proceedings of Logic in Computer Science (LICS ’22), page 13 pages. ACM, 2022.  doi:10.1145/3531130.3533361.
  * [Asc11] Federico Aschieri.  Learning, Realizability and Games in Classical Arithmetic.  PhD thesis, Università degli Studi di Torino and Queen Mary, University of London, 2011.  doi:10.48550/arXiv.1012.4992.
  * [Atk09] Robert Atkey.  Parameterised notions of computation.  Journal of Functional Programming, 19(3&4):335–376, 2009.  doi:10.1017/S095679680900728X.
  * [Bd09] Stefano Berardi and Ugo de’Liguoro.  Toward the interpretation of non-constructive reasoning as non-monotonic learning.  Information and Computation, 207(1):63–81, 2009.  doi:10.1016/j.ic.2008.10.003.
  * [Ber04] Ulrich Berger.  A computational interpretation of open induction.  In Proceedings of Logic in Computer Science (LICS ’04), pages 326–334. IEEE, 2004.
  * [Bir12] Giovanni Birolo.  Interactive Realizability, Monads and Witness Extraction.  PhD thesis, Università degli Studi di Torino, 2012.  doi:https://doi.org/10.48550/arXiv.1304.4091.
  * [BSW14] Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods.  Extracting imperative programs from proofs: In-place quicksort.  In Proceedings of Types for Proofs and Programs (TYPES’13), volume 26 of LIPIcs, pages 84–106, 2014.  doi:10.4230/LIPIcs.TYPES.2013.84.
  * [BT21] Ulrich Berger and Hideki Tsuiki.  Intuitionistic fixed point logic.  Annals of Pure and Applied Logic, 172:102903, 2021.  doi:0.1016/j.apal.2020.102903.
  * [CLM13] Martin Churchill, James Laird, and Guy McCusker.  Imperative programs as proofs via game semantics.  Annals of Pure and Applied Logic, 164(11):1038–1078, 2013.  doi:10.1016/j.apal.2013.05.005.
  * [CMM+09] Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky.  Effective interactive proofs for higher-order imperative programs.  In Proceedings of International Conference on Functional Programming (ICFP’09), pages 79–90. ACM, 2009.  doi:10.1145/1596550.1596565.
  * [DF89] Olivier Danvy and Andrzej Filinski.  A functional abstraction of typed contexts.  Technical Report 89/12, BRICS, 1989.
  * [DLR15] Norman Danner, Dan Licata, and Ramyaa Ramyaa.  Denotational cost semantics for functional languages with inductive types.  In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pages 140–151, 2015.  doi:10.1145/2784731.2784749.