Jonas Frey

# Realizability Toposes from Specifications 111 This work is supported by the
Danish Council for Independent Research Sapere Aude grant “Complexity through
Logic and Algebra” (COLA).

Jonas Frey  Department of Computer Science
University of Copenhagen, Denmark
<EMAIL_ADDRESS>
###### Abstract

We investigate a framework of Krivine realizability with I/O effects, and
present a method of associating realizability models to _specifications_ on
the I/O behavior of processes, by using adequate interpretations of the
central concepts of _pole_ and _proof-like term_. This method does in
particular allow to associate realizability models to computable functions.

Following recent work of Streicher and others we show how these models give
rise to _triposes_ and _toposes_.

##  1 Introduction

Krivine realizability with side effects has been introduced by Miquel in [14].
In this article we demonstrate how an instance of Miquel’s framework including
I/O instructions allows to associate _realizability toposes_ to
_specifications_ , i.e. sets of requirements imposed on the I/O behavior of
programs. Since the requirement to compute a specific function $f$ can be
viewed as a specification, we do in particular obtain a way to _associate
toposes to computable functions_.

These toposes are different from traditional ‘Kleene’ realizability toposes
such as the _effective topos_ [6] in that we associate toposes to _individual_
computable functions, whereas the effective topos incorporates _all_ recursive
functions on equal footing. Another difference to the toposes based on Kleene
realizability is that the internal logic of the latter is _constructive_ ,
whereas the present approach is based on Krivine’s realizability
interpretation [10], which validates classical logic.

To represent specifications we make use of the fact that Krivine’s
realizability interpretation is parametric over a set of processes called the
_pole_. The central observation (Lemma 5.21 and Theorem 5.23) is that non-
trivial specifications on program behavior give rise to poles leading to
consistent (i.e. non-degenerate) interpretations.

To give a categorical account of Krivine realizability we follow recent work
of Streicher [18] and others [17, 20, 2], which demonstrates how Krivine
realizability models give rise to _triposes_. Toposes are then obtained via
the tripos-to-topos construction [7].

Our basic formalism is an extension of the Krivine machine (2) that gives an
operational semantics to I/O instructions for single bits. We give two
formulations of the operational semantics – one (4) in terms of a transition
relation on processes including a _state_ (which is adequate for reasoning
about function computation), and one (7) in terms of a labeled transition
system admitting to reason about program equivalence in terms of bisimulation.
The two operational semantics are related by Corollary 3.8, which we use to
prove a Turing completeness result in Theorem 4.8.

###  1.1 Related work

The idea of adding instructions with new evaluation rules to the machine plays
a central role in Krivine’s writings, as a means to realize non-logical
axioms. Citing from [11]:

> _“Indeed, when we realize usual axioms of mathematics, we need to introduce,
> one after the other, the very standard tools in system programming: for the
> law of Peirce, these are continuations (particularly useful for exceptions);
> for the axiom of dependent choice, these are the clock and the process
> numbering; for the ultrafilter axiom and the well ordering of $\mathbb{R}$,
> these are no less than I/O instructions on a global memory, in other words
> assignment.”_

Although features like exceptions and memory are often called  _effects_ , it
is arguable whether they should be called  _side_ effects, since they do not
interact with the outside world.

The idea to add instructions for _side_ effects which are influenced by – and
influence – the outside world,p has already been investigated by Miquel [14,
Section 2.2], and our execution relation (4) can be viewed as an instance of
his framework.

What sets the present approach apart is that Miquel views the state of the
world (represented by a forcing condition) as being _part_ of a process and
requires poles to be saturated w.r.t. all (including effectful) reductions,
whereas for us poles are sets of ‘bare’ processes without state, which are
saturated only w.r.t. reduction free of side-effects.

This difference is crucial in that it enables the construction of poles from
specifications.

##  2 Syntax and machine

In this section we recall Krivine’s abstract machine with continuations as
described in [10]. We then go on to describe an extension of the syntax by I/O
instructions, and describe an operational semantics as a transition relation
on triples $(p,\iota,o)$ of process, input, and output.

###  2.1 Krivine’s machine

We recall the underlying syntax and machine of Krivine’s classical
realizability from [10]. The syntax consists of three syntactic classes called
_terms, stacks_ , and _processes_.

Terms: |  $t$ $\;::=\;$ | $x\mathrel{|}\lambda x\\!\,.\,\\!t\mathrel{|}t{}\,t\mathrel{|}\mathsf{c\\!c}\mathrel{|}\mathsf{k}_{\pi}$ |
---|---|---|---
Stacks: |  $\pi$ $\;::=\;$ | $\pi_{0}\mathrel{|}t\mathclose{\cdot}\pi$ |  $t$ closed, $\pi_{0}\in\mathsf{\Pi}_{0}$
Processes: |  $p$ $\;::=\;$ | $t\star\pi$ |  $t$ closed
(1)

Thus, the terms are the terms of the $\lambda$-calculus, augmented by a
constant $\mathsf{c\\!c}$ for call/cc, and continuation terms
$\mathsf{k}_{\pi}$ for any stack $\pi$. A stack, in turn, is a list of closed
terms terminated by an element $\pi_{0}$ of a designated set
$\mathsf{\Pi}_{0}$ of _stack constants_. A process is a pair $t\star\pi$ of a
closed term and a stack. The set of closed terms is denoted by
$\mathsf{\Lambda}$, the set of stacks is $\mathsf{\Pi}$, and the set of
processes is $\mathsf{\mathsf{\Lambda}\\!\star\\!\mathsf{\Pi}}$.

Krivine’s machine is now defined by a transition relation $\succ$ on processes
called _evaluation_.

(push) |  $tu$$\;\star\;$ |  $\pi$ $\quad\succ\quad$ |  $t$$\;\star\;$ | $u\mathclose{\cdot}\pi$
---|---|---|---|---
(pop) |  $(\lambda x\,.\,t[x])$$\;\star\;$ |  $u\mathclose{\cdot}\pi$ $\quad\succ\quad$ |  $t[u]$$\;\star\;$ | $\pi$
(save) |  $\mathsf{c\\!c}$$\;\star\;$ |  $t\mathclose{\cdot}\pi$ $\quad\succ\quad$ |  $t$$\;\star\;$ | $\mathsf{k}_{\pi}\mathclose{\cdot}\pi$
(restore) |  $\mathsf{k}_{\pi}$$\;\star\;$ |  $t\mathclose{\cdot}\rho$ $\quad\succ\quad$ |  $t$$\;\star\;$ | $\pi$
(2)

The first two rules implement _weak head reduction_ of $\lambda$-terms, and
the third and fourth rule capture and restore continuations.

###  2.2 The machine with I/O

To incorporate I/O we modify the syntax as follows:

$\begin{array}[]{ll@{\;::=\;}l@{\qquad}l}\text{Terms:}&t&x\mathrel{|}\lambda
x\\!\,.\,\\!t\mathrel{|}t{}\,t\mathrel{|}\mathsf{c\\!c}\mathrel{|}\mathsf{k}_{\pi}\mathrel{|}\mathsf{r}\mathrel{|}\mathsf{w\\!1}\mathrel{|}\mathsf{w\\!0}\mathrel{|}\mathsf{end}\\\
\text{Stacks:}&\pi&\varepsilon\mathrel{|}t\mathclose{\cdot}\pi&t\text{
closed}\\\ \text{Processes:}&p&t\star\pi\mathrel{|}\top&t\text{
closed}\end{array}$ (3)

The grammar for terms is extended by constants
$\mathsf{r},\mathsf{w\\!0},\mathsf{w\\!1},\mathsf{end}$ for reading, writing
and termination, and in exchange the stack constants are omitted –
$\varepsilon$ is the empty stack. Finally there is a _process constant_ $\top$
also representing termination – the presence of both $\mathsf{end}$ and $\top$
will be important in Section 3.

We write $\mathsf{\Lambda}_{e}$ and $\mathsf{\Pi}_{e}$ for the sets of terms
and stacks of the syntax with I/O, and $\mathsf{P}$ for the set of processes.
Furthermore, we denote by $\mathsf{\Lambda}_{p}$ the set of _pure_ terms, i.e.
terms not containing any of
$\mathsf{r},\mathsf{w\\!0},\mathsf{w\\!1},\mathsf{end}$.

The operational semantics of the extended syntax is given in terms of
_execution contexts_ , which are triples $(p,\iota,o)$ of a process $p$, and a
pair $\iota,o\in\\{0,1\\}^{*}$ of binary strings representing input and
output. On these execution contexts, we define the _execution relation_
$\leadsto$ as follows:

$\begin{array}[]{c@{\qquad(}r@{\;\star\;}r@{,\;}r@{,\;}r@{)\quad\kexec\quad(}r@{\;\star\;}r@{,\;}r@{,\;}r@{)\qquad}l}(\tau)&t&\pi&\iota&o)\quad\leadsto&u&\rho&\iota&o&\text{whenever
}t\star\pi\succ u\star\rho\\\
(\mathsf{r0})&\mathsf{r}&t\mathclose{\cdot}u\mathclose{\cdot}v\mathclose{\cdot}\pi&0\iota&o)\quad\leadsto&t&\pi&\iota&o\\\
(\mathsf{r1})&\mathsf{r}&t\mathclose{\cdot}u\mathclose{\cdot}v\mathclose{\cdot}\pi&1\iota&o)\quad\leadsto&u&\pi&\iota&o\\\
(\mathsf{r\varepsilon})&\mathsf{r}&t\mathclose{\cdot}u\mathclose{\cdot}v\mathclose{\cdot}\pi&\varepsilon&o)\quad\leadsto&v&\pi&\varepsilon&o\\\
(\mathsf{w0})&\mathsf{w\\!0}&t\mathclose{\cdot}\pi&\iota&o)\quad\leadsto&t&\pi&\iota&0o\\\
(\mathsf{w1})&\mathsf{w\\!1}&t\mathclose{\cdot}\pi&\iota&o)\quad\leadsto&t&\pi&\iota&1o\\\
(\mathsf{e})&\mathsf{end}&\pi&\iota&o)\quad\leadsto&\lx@intercol\top\hfil,\;&\iota&o\\\
\end{array}$ (4)

Thus, if there is neither of
$\mathsf{r},\mathsf{w\\!0},\mathsf{w\\!1},\mathsf{end}$ in head position, the
process is reduced as in (2) without changing $\iota$ and $o$. If $\mathsf{r}$
is in head position, the computation selects one of the first three arguments
depending on whether the input starts with a $0$, a $1$, or is empty.
$\mathsf{w\\!0}$ and $\mathsf{w\\!1}$ write out $0$ and $1$, and
$\mathsf{end}$ discards the stack and yields $\top$, which represents
successful termination.

We observe that the execution relation is _deterministic_ , i.e. for every
execution context there is at most one transition possible, which is
determined by the term in head position, and in case of $\mathsf{r}$ also by
the input.

###  2.3 Representing functions

We view the above formalism as a model of computation that explicitly includes
reading of input, and writing of output.

Consequently, when thinking about expressivity we are not so much interested
in the ability of the machine to transform abstract representations of data
like ‘Church numerals’, but rather in the functions on binary strings that
processes can compute by reading their argument from the input, and writing
the result to the output.

######  Definition 2.1.

For $n\in\mathbb{N}$, $\mathrm{bin}(n)\in\\{0,1\\}^{*}$ is the base $2$
representation of $n$. $0$ is represented by the empty string, thus we have
e.g. $\mathrm{bin}(0)=\varepsilon$, $\mathrm{bin}(1)=1$, $\mathrm{bin}(2)=10$,
$\mathrm{bin}(3)=11$, …

A process $p$ is said to _implement_ a partial function
$f:\mathbb{N}\rightharpoonup\mathbb{N}$, if
$(p,\mathrm{bin}(n),\varepsilon)\leadsto^{*}(\top,\varepsilon,\mathrm{bin}(f(n)))$
for all $n\in\mathrm{dom}(f)$.

######  Remark 2.2.

There is a stronger version of the previous definition which requires
$(p,\mathrm{bin}(n),\varepsilon)$ to diverge or block for
$n\not\in\mathrm{dom}(f)$, and a completeness result like Thm. 4.8 can be
shown for the strengthened definition as well.

We use the weaker version, since we expect the poles $\Bot_{f}$ defined in
Section 5.2.1 to be better behaved this way.

###  2.4 $\beta$-reduction

To talk about contraction of single $\beta$-redexes which are not necessarily
in head position in a process $p$, we define _contexts_ – which are
terms/stacks/processes with a single designated hole $[\cdot]$ in term
position – by the following grammar:

Term contexts: |  $t[\cdot]$$\quad::=\quad$ | $[\cdot]\mathrel{|}\lambda x\\!\,.\,\\!t[\cdot]\mathrel{|}t[\cdot]{}\,t\mathrel{|}t\,t[\cdot]\mathrel{|}\mathsf{k}_{\pi[\cdot]}$ |
---|---|---|---
Stack contexts: |  $\pi[\cdot]$$\quad::=\quad$ | $t\mathclose{\cdot}\pi[\cdot]\mathrel{|}t[\cdot]\mathclose{\cdot}\pi$ |  $t$,$t[\cdot]$ closed
Process contexts: |  $p[\cdot]$$\quad::=\quad$ | $t[\cdot]\star\pi\mathrel{|}t\star\pi[\cdot]$ |
(5)

Contexts are used to talk about substitution that allows capturing of
variables – as described in [1, 2.1.18], given a context
$t[\cdot]$/$\pi[\cdot]$/$p[\cdot]$ and a term $u$, $t[u]$/$\pi[u]$/$p[u]$ is
the result of replacing the hole $[\cdot]$ in
$t[\cdot]$/$\pi[\cdot]$/$p[\cdot]$ by $u$, allowing potential free variables
in $u$ to be captured. We say that $u$ is _admissible_ for
$t[\cdot]$/$\pi[\cdot]$/$p[\cdot]$, if $t[u]$/$\pi[u]$/$p[u]$ is a valid
term/stack/process conforming to the closedness condition for terms making up
stacks.

Now we can express $\beta$-reduction as the action of contracting a single
redex: given a redex $(\lambda x\,.\,u)v$ which is admissible for a context
$t[\cdot]$/$\pi[\cdot]$/$p[\cdot]$, we have

$t[(\lambda x\,.\,u)v]\to_{\beta}t[u[v/x]]\qquad\pi[(\lambda
x\,.\,u)v]\to_{\beta}\pi[u[v/x]]\qquad p[(\lambda
x\,.\,u)v]\to_{\beta}p[u[v/x]],$ (6)

and any single $\beta$-reduction can uniquely be written this way.
$\beta$-equivalence $\simeq_{\beta}$ is the equivalence relation generated by
$\beta$-reduction.

##  3 Bisimulation and $\top$-equivalence

To reason efficiently about execution of processes with side effects – in
particular to show Turing completeness in Section 4 – we want to show that
although the computation model imposes a deterministic reduction strategy, we
can perform $\beta$-reduction anywhere in a process without changing its I/O
behavior.

The natural choice of concept to capture ‘equivalence of I/O behavior’ is
_weak bisimilarity_ (see [13, Section 4.2]), and in order to make this
applicable to processes we have to reformulate the operational semantics as a
_labeled transition system_ (LTS).

We use the set
$\mathcal{L}=\\{\mathsf{r0},\mathsf{r1},\mathsf{r\varepsilon},\mathsf{w0},\mathsf{w1},\mathsf{e}\\}$
of labels, where $\mathsf{r0}$, $\mathsf{r1}$ represent reading of a $0$ or
$1$, respectively, and $\mathsf{w0}$, $\mathsf{w1}$ represent writing of bits.
$\mathsf{r\varepsilon}$ represents the unsuccessful attempt of reading on
empty input, and $\mathsf{e}$ represents successful termination. The set
$\mathit{Act}=\mathcal{L}\cup\\{\tau\\}$ of _actions_ contains the labels as
well as the symbol $\tau$ representing a ‘silent’ transition, that is used to
represent effect-free evaluation.

The transition system on processes is now given as follows.

$\begin{array}[]{r@{\,\star\,}l @{\,\,}c@{\,\,}
r@{\,\star\,}l@{\qquad}r@{\,\star\,}l @{\,\,}c@{\,\,}
r@{\,\star\,}l@{\qquad}r@{\,\star\,}l @{\,\,}c@{\,\,} r@{\,\star\,}l}(\lambda
x\,.\,t[x])&t\mathclose{\cdot}\pi&\xrightarrow{\tau}&t[u]&\pi&\mathsf{r}&t\mathclose{\cdot}u\mathclose{\cdot}v\mathclose{\cdot}\pi&\xrightarrow{\mathsf{r0}}&t&\pi&\mathsf{w\\!0}&t\mathclose{\cdot}\pi&\xrightarrow{\mathsf{w0}}&t&\pi\\\
tu&\pi&\xrightarrow{\tau}&t&u\mathclose{\cdot}\pi&\mathsf{r}&t\mathclose{\cdot}u\mathclose{\cdot}v\mathclose{\cdot}\pi&\xrightarrow{\mathsf{r1}}&u&\pi&\mathsf{w\\!1}&t\mathclose{\cdot}\pi&\xrightarrow{\mathsf{w1}}&t&\pi\\\
\mathsf{c\\!c}&t\mathclose{\cdot}\pi&\xrightarrow{\tau}&t&\mathsf{k}_{\pi}\mathclose{\cdot}\pi&\mathsf{r}&t\mathclose{\cdot}u\mathclose{\cdot}v\mathclose{\cdot}\pi&\xrightarrow{\mathsf{r\varepsilon}}&v&\pi&\mathsf{end}&\pi&\xrightarrow{\mathsf{e}}&\lx@intercol\top\hfil\;\\\
\mathsf{k}_{\pi}&t\mathclose{\cdot}\rho&\xrightarrow{\tau}&t&\pi\end{array}$
(7)

Observe that the $\tau$-transitions are in correspondence with the transitions
of the evaluation relation (2), and the labeled transitions correspond to the
remaining transitions of the execution relation (4).

We now recall the definition of _weak bisimulation relation_ from [13, Section
4.2].

######  Definition 3.1.

  * •

For processes $p,q$ we write $p\xRightarrow{\tau}q$ for
$p\xrightarrow{\tau}^{\raisebox{-3.0pt}{$\scriptstyle*$}}q$, and for
$\alpha\neq\tau$ we write $p\xRightarrow{\alpha}q$ for $\exists
p^{\prime},q^{\prime}\,.\,p\xRightarrow{\tau}p^{\prime}\xrightarrow{\alpha}q^{\prime}\xRightarrow{\tau}q$.

  * •

A _weak bisimulation_ on $\mathsf{P}$ is a binary relation
$R\subseteq\mathsf{P}^{2}$ such that for all $\alpha\in\mathit{Act}$ and
$(p,q)\in R$ we have

$\displaystyle p\xrightarrow{\alpha}p^{\prime}$
$\displaystyle\quad\Rightarrow\quad\exists
q^{\prime}\,.\,q\xRightarrow{\alpha}q^{\prime}\,\wedge\,(p^{\prime},q^{\prime})\in
R\quad\text{and}$ (8) $\displaystyle q\xrightarrow{\alpha}q^{\prime}$
$\displaystyle\quad\Rightarrow\quad\exists
p^{\prime}\,.\,p\xRightarrow{\alpha}p^{\prime}\,\wedge\,(p^{\prime},q^{\prime})\in
R.$

  * •

Two processes $p,q$ are called _weakly bisimilar_ (written $p\approx q$), if
there exists a weak bisimulation relation $R$ with $(p,q)\in R$.

We recall the following important properties of the weak bisimilarity relation
$\approx$.

######  Lemma 3.2.

Weak bisimilarity is itself a weak bisimulation, and furthermore it is an
equivalence relation.

######  Proof 3.3.

[13, Proposition 4.2.7]

To show that $\beta$-equivalent processes are bisimilar, we have to find a
bisimulation relation containing $\beta$-equivalence. The following relation
does the job.

######  Definition 3.4 ($\gamma$-equivalence).

$\gamma$-equivalence (written $p\simeq_{\gamma}q$) is the equivalence relation
on processes that is generated by $\beta$-reduction and $\tau$-transitions.

######  Lemma 3.5.

$\gamma$-equivalence of processes is a weak bisimulation.

######  Proof 3.6.

It is sufficient to verify conditions (8) on the generators of
$\gamma$-equivalence, i.e. one-step $\beta$-reductions and $\tau$-transitions.
Therefore we show the following:

  1. 1.

if $p\xrightarrow{\tau}q$ and $p\xrightarrow{\alpha}p^{\prime}$ then there
exists $q^{\prime}$ with $q\xRightarrow{\alpha}q^{\prime}$ and
$p^{\prime}\simeq_{\gamma}q^{\prime}$

  2. 2.

if $p\xrightarrow{\tau}q$ and $q\xrightarrow{\alpha}q^{\prime}$ then there
exists $p^{\prime}$ with $p\xRightarrow{\alpha}p^{\prime}$ and
$p^{\prime}\simeq_{\gamma}q^{\prime}$

  3. 3.

if $p\to_{\beta}q$ and $p\xrightarrow{\alpha}p^{\prime}$ then there exists
$q^{\prime}$ with $q\xRightarrow{\alpha}q^{\prime}$ and
$p^{\prime}\simeq_{\gamma}q^{\prime}$

  4. 4.

if $p\to_{\beta}q$ and $q\xrightarrow{\alpha}q^{\prime}$ then there exists
$p^{\prime}$ with $p\xRightarrow{\alpha}p^{\prime}$ and
$p^{\prime}\simeq_{\gamma}q^{\prime}$

In the first case, the fact that the LTS can only branch if $\mathsf{r}$ is in
head position, and this does not involve $\tau$-transitions, implies that
$\alpha=\tau$ and $p^{\prime}=q$, and we can choose $q^{\prime}=q$ as well. In
the second case we have $p\xRightarrow{\alpha}q^{\prime}$ and thus can choose
$p^{\prime}=q^{\prime}$.

For cases 3 and 4, which we treat simultaneously, we have to analyze the
structure of $p$ and $q$, which are of the form $r[(\lambda x\,.\,s)t]$ and
$r[s[t/x]]$ for some context $r[\cdot]$ (see Section 2.4). The proof proceeds
by cases on the structure of $r[\cdot]$.

If $r[\cdot]$ is of either of the forms $(st\star\pi)[\cdot]$222The notation
is meant to convey that we don’t care if the hole is in $s$, $t$, or $\pi$.,
$\mathsf{w\\!0}\star\pi[\cdot]$, $\mathsf{w\\!1}\star\pi[\cdot]$,
$\mathsf{c\\!c}\star\pi[\cdot]$, $(\mathsf{k}_{\pi}\star\rho)[\cdot]$, or
$\mathsf{end}\star\pi[\cdot]$, then it is immediately evident that $p$ and $q$
can perform the same unique transition (if any), and the results will again be
$\beta$-equivalent (possibly trivially, since the redex can get deleted in the
transition).

If $r[\cdot]$ is of the form $((\lambda y\,.\,u)\star\pi)[\cdot]$ then this is
true as well, regardless of whether the hole is in $u$ or in $\pi$ (here the
redex can be duplicated, if the hole is in the first term in $\pi$).

If $r[\cdot]$ is of the form $\mathsf{r}\star\pi[\cdot]$ then several
transitions may be possible, but any transition taken by either of $p$ or $q$
can also be taken by the other, and the results will again be
$\beta$-equivalent.

It remains to consider $r[\cdot]$ of the form $[\cdot]\star\pi$. In this case,
$p=(\lambda x\,.\,s)t\star\pi$ and $q=s[t/x]\star\pi$. Here $p$ can perform
the transition $p\xrightarrow{\tau}(\lambda x\,.\,s)\star
t\mathclose{\cdot}\pi$ which can be matched by $q\xRightarrow{\tau}q$ where we
have $(\lambda x\,.\,s)\star
t\mathclose{\cdot}\pi\simeq_{\gamma}p\simeq_{\gamma}q$. In the other direction
we have $p\xRightarrow{\alpha}q^{\prime}$ for every
$q\xrightarrow{\alpha}q^{\prime}$ since $p\xRightarrow{\tau}q$.

The following definition and corollary makes the link between the execution
relation (4) and the LTS (7).

######  Definition 3.7.

Two execution contexts $(p,\iota,o)$, $(q,\iota^{\prime},o^{\prime})$ are
called _$\top$ -equivalent_ (written
$(p,\iota,o)\sim_{\top}(q,\iota^{\prime},o^{\prime})$), if for all
$\iota^{\prime\prime},o^{\prime\prime}\in\\{0,1\\}^{*}$ we have

$(p,\iota,o)\leadsto^{*}(\top,\iota^{\prime\prime},o^{\prime\prime})\quad\text{iff}\quad(q,\iota^{\prime},o^{\prime})\leadsto^{*}(\top,\iota^{\prime\prime},o^{\prime\prime}).$

######  Corollary 3.8.

  1. 1.

$p\approx q$ implies $(p,\iota,o)\sim_{\top}(q,\iota,o)$ for all
$\iota,o\in\\{0,1\\}^{*}$.

  2. 2.

$(p,\iota,o)\leadsto^{*}(q,\iota^{\prime},o^{\prime})$ implies
$(p,\iota,o)\sim_{\top}(q,\iota^{\prime},o^{\prime})$.

  3. 3.

$(p,\iota,o)\sim_{\top}(\top,\iota^{\prime},o^{\prime})$ implies
$(p,\iota,o)\leadsto^{*}(\top,\iota^{\prime},o^{\prime})$.

######  Proof 3.9.

For the first claim we show that

$p\approx
q,\quad(p,\iota,o)\leadsto^{*}(\top,\iota^{\prime},o^{\prime})\quad\text{implies}\quad(q,\iota,o)\leadsto^{*}(\top,\iota^{\prime},o^{\prime})$

by induction on the length of
$(p,\iota,o)\leadsto^{*}(\top,\iota^{\prime},o^{\prime})$. The base case is
clear. For the induction step assume that
$(p,\iota,o)\rightsquigarrow(p^{*},\iota^{*},o^{*})\leadsto^{*}(\top,\iota^{\prime},o^{\prime})$.
If the initial transition is a $(\tau)$ in the execution relation (4), then
have $p^{*}\cong q$, $\iota^{*}=\iota$ and $o^{*}=o$, and we can apply the
induction hypothesis. If the initial transition corresponds to another clause
in (4), then there is a corresponding transition $p\xrightarrow{\alpha}q$ with
$\alpha\in\mathcal{L}$ in the LTS (7), and by bisimilarity there exists a
$q^{*}$ with $q\xRightarrow{\alpha}q^{*}$ and $p^{*}\approx q^{*}$. Now the
induction hypothesis implies
$(q^{*},\iota^{*},o^{*})\leadsto^{*}(\top,\iota^{\prime},o^{\prime})$, and
from $q\xRightarrow{\alpha}q^{*}$ we can deduce
$(q,\iota,o)\leadsto^{*}(q^{*},\iota^{*},o^{*})$ by cases on $\alpha$.

The second claim follows since $\rightsquigarrow$ is deterministic.

The third claim follows since $(\top,\iota^{\prime},o^{\prime})$ can not
perform any more transitions.

##  4 Expressivity

In this section we show that the machine with I/O is Turing complete, i.e.
that every computable $f:\mathbb{N}\rightharpoonup\mathbb{N}$ can be
implemented in the sense of Def. 2.1 by a process $p$.

Roughly speaking, given $f$, we define a process $p$ that reads the input,
transforms it into a Church numeral, applies a term $t$ that computes $f$ on
the level of Church numerals, and then writes the result out.

To decompose the task we define terms $R$ and $W$ for reading and writing,
with the properties that
$(R\ast\pi,\mathrm{bin}(n),o)\sim_{\top}(\overline{n}\star\pi,\varepsilon,o)$
($\overline{n}$ is the $n$-th Church numeral), and
$(W\overline{n}\ast\pi,\iota,\varepsilon)\sim_{\top}(\top,\iota,\mathrm{bin}(n))$
for all $n\in\mathbb{N}$.

Now the naive first attempt to combine $R$ and $W$ with the term $t$ computing
the function would be something like $W(tR)$, but this would only work if the
operational semantics was call by value. The solution is to use Krivine’s
_storage operators_ [9] which where devised precisely to simulate call by
value in call by name, and we use a variation of them.

The following definition introduces the terms $R$ and $W$, after giving some
auxiliary definitions.

######  Definition 4.1.

$E,Z,B,C,H,Y,S$ are $\lambda$-terms satisfying

$\begin{array}[]{l@{\,\,\bequiv\,\,}l@{\qquad}l@{\,\,\bequiv\,\,}l@{\qquad}l@{\,\,\bequiv\,\,}l}B\,\overline{n}\hfil\,\,\simeq_{\beta}&\overline{2n}&E\,\overline{(2n)}\,s\,t\hfil\,\,\simeq_{\beta}&s&Y\,t\hfil\,\,\simeq_{\beta}&t\,(Y\,t)\\\
C\,\overline{n}\hfil\,\,\simeq_{\beta}&\overline{2n+1}&E\,\overline{(2n+1)}\,s\,t\hfil\,\,\simeq_{\beta}&t\\\
H\,\overline{n}\hfil\,\,\simeq_{\beta}&\overline{\mathrm{floor}(n/2)}&Z\,\overline{(0)}\,s\,t\hfil\,\,\simeq_{\beta}&s\\\
S\,\overline{n}\hfil\,\,\simeq_{\beta}&\overline{n+1}&Z\,\overline{(n+1)}\,s\,t\hfil\,\,\simeq_{\beta}&t\end{array}\qquad$
(9)

for all terms $s,t$ and $n\in\mathbb{N}$, where $\overline{n}$ is the Church
numeral $\lambda fx\,.\,f^{n}x$.333Such terms exist by elementary
$\lambda$-calculus, see e.g. [5, Chapters 3,4]. In particular, $Y$ is known as
_fixed point operator_.

The terms $F$, $R$, $W$ are defined as follows:

$\begin{array}[]{l@{\,\,=\,\,}l@{\qquad}l@{\,\,\bequiv\,\,}l@{\qquad}l@{\,\,\bequiv\,\,}l}F&\lambda
hy\,.\,h(S\,y)\\\ R&Y{Q}\,\overline{0}\quad\text{where}\quad{Q}=\lambda
xn\,.\,\mathsf{r}(x(B\,n))(x(C\,n))n\\\ W&YV\quad\text{where}\quad V=\lambda
xn\,.\,Z\,n\,\mathsf{end}(E\,n(\mathsf{w\\!0}\,x(H\,n))(\mathsf{w\\!1}\,x(H\,n)))\end{array}$
(10)

The next three lemmas explain the roles of the terms $R,F$, and $W$.

######  Lemma 4.2.

For all $n\in\mathbb{N}$, $\pi\in\mathsf{\Pi}$ and $o\in\\{0,1\\}^{*}$ we have
$(R\star\pi,\mathrm{bin}(n),o)\sim_{\top}(\overline{n}\star\pi,\varepsilon,o)$.

######  Proof 4.3.

For all $n\in\mathbb{N}$ we have
$YQ\,\overline{n}\simeq_{\beta}Q(YQ)\overline{n}\simeq_{\beta}\mathsf{r}(YQ\overline{(2n)})(YQ\overline{(2n+1)})\overline{n}$,
and thus

$\begin{array}[]{l@{\,\,\tequiv\,\,}l}(YQ\,\overline{n}\star\pi,\varepsilon,o)\hfil\,\,\sim_{\top}&(\overline{n}\star\pi,\varepsilon,o)\\\
(YQ\,\overline{n}\star\pi,0\iota,o)\hfil\,\,\sim_{\top}&(YQ\,\overline{(2n)}\star\pi,\iota,o)\\\
(YQ\,\overline{n}\star\pi,1\iota,o)\hfil\,\,\sim_{\top}&(YQ\,\overline{(2n+1)}\star\pi,\iota,o)\\\
\end{array}$ (11)

The claim follows by induction on the length of $\mathrm{bin}(n)$, since
$\mathrm{bin}(2n)=\mathrm{bin}(n)0$ for $n>0$, and
$\mathrm{bin}(2n+1)=\mathrm{bin}(n)1$.

######  Lemma 4.4.

For $n\in\mathbb{N}$ and $t$ any closed term, we have
$\overline{n}\,F\,t\,\overline{0}\simeq_{\beta}t\,\overline{n}$.

######  Proof 4.5.

This is because
$\overline{n}\,F\,t\overline{0}\simeq_{\beta}F^{n}\,t\,\overline{0}\simeq_{\beta}t\,(S^{n}\overline{0})\simeq_{\beta}t\,\overline{n}$,
where the second step can be shown by induction on $n$.

######  Lemma 4.6.

For all $n\in\mathbb{N}$, $\pi\in\mathsf{\Pi}$ and $\iota\in\\{0,1\\}^{*}$ we
have
$(W\overline{n}\star\pi,\iota,\varepsilon)\sim_{\top}(\top,\iota,\mathrm{bin}{(n)})$.

######  Proof 4.7.

We have
$W\,\overline{n}\simeq_{\beta}V\,W\,\overline{n}\simeq_{\beta}Z\,\overline{n}\,\mathsf{end}(E\,\overline{n}(\mathsf{w\\!0}\,W(H\,\overline{n}))(\mathsf{w\\!1}\,W(H\,\overline{n})))$,
and therefore

$\begin{array}[]{l@{\,\,\tequiv\,\,}l@{\,\,\tequiv\,\,}l}(W\,\overline{0}\star\pi,\iota,o)\hfil\,\,\sim_{\top}&(\mathsf{end}\star\pi,\iota,o)\hfil\,\,\sim_{\top}&(\top,\iota,o)\\\
(W\,\overline{(2n)}\star\pi,\iota,o)\hfil\,\,\sim_{\top}&(\mathsf{w\\!0}\,W(H\,\overline{(2n)})\star\pi,\iota,o)\hfil\,\,\sim_{\top}&(W(\overline{n})\star\pi,\iota,0o)\quad\text{for
}(n>0)\\\
(W\,\overline{(2n+1)}\star\pi,\iota,o)\hfil\,\,\sim_{\top}&(\mathsf{w\\!1}\,W(H\,\overline{(2n+1)})\star\pi,\iota,o)\hfil\,\,\sim_{\top}&(W(\overline{n})\star\pi,\iota,1o).\end{array}$
(12)

The claim follows again by induction on the length of $\mathrm{bin}(n)$.

######  Theorem 4.8.

Every computable function $f:\mathbb{N}\rightharpoonup\mathbb{N}$ can be
implemented by a process $p$.

######  Proof 4.9.

From [5, Thm. 4.23] we know that there exists a term $t$ with
$t\,\overline{n}\simeq_{\beta}\overline{f(n)}$ for $n\in\mathrm{dom}(f)$. The
process $p$ is given by $R\star
F\mathclose{\cdot}t\mathclose{\cdot}\overline{0}\mathclose{\cdot}F\mathclose{\cdot}W\mathclose{\cdot}\overline{0}$.
Indeed, for $n\in\mathrm{dom}(f)$ we have

$\begin{array}[]{l@{\,\,\tequiv\,\,}l@{\,\,\tequiv\,\,}l}(R\star
F\mathclose{\cdot}t\mathclose{\cdot}\overline{0}\mathclose{\cdot}F\mathclose{\cdot}W\mathclose{\cdot}\overline{0},\mathrm{bin}(n),\varepsilon)\hfil\,\,\sim_{\top}&(\overline{n}\star
F\mathclose{\cdot}t\mathclose{\cdot}\overline{0}\mathclose{\cdot}F\mathclose{\cdot}W\mathclose{\cdot}\overline{0},\varepsilon,\varepsilon)\hfil\,\,\sim_{\top}&(\overline{n}\,Ft\overline{0}\star
F\mathclose{\cdot}W\mathclose{\cdot}\overline{0},\varepsilon,\varepsilon)\\\
\hfil\,\,\sim_{\top}&(t\,\overline{n}\star
F\mathclose{\cdot}W\mathclose{\cdot}\overline{0},\varepsilon,\varepsilon)\hfil\,\,\sim_{\top}&(\overline{f(n)}\star
F\mathclose{\cdot}W\mathclose{\cdot}\overline{0},\varepsilon,\varepsilon)\\\
\hfil\,\,\sim_{\top}&(W\,\overline{f(n)}\star\varepsilon,\varepsilon,\varepsilon)\hfil\,\,\sim_{\top}&(\top,\varepsilon,\mathrm{bin}(f(n)))\end{array}$
(13)

and we deduce $(R\star
F\mathclose{\cdot}t\mathclose{\cdot}\overline{0}\mathclose{\cdot}F\mathclose{\cdot}W\mathclose{\cdot}\overline{0},\mathrm{bin}(n),\varepsilon)\leadsto^{*}(\top,\varepsilon,\mathrm{bin}(f(n)))$
by Corollary 3.8-3.

##  5 Realizability and triposes

The aim of this section is to describe how the presence of I/O instructions
allows to define new realizability models, which we do in the categorical
language of triposes and toposes [21].

In Subsection 5.1 we give a categorical reading of Krivine’s realizability
interpretation as described in [10] and show how it gives rise to triposes. In
Subsection 5.2 we show how the definitions can be adapted to the syntax and
machine with I/O, and how this allows us to define new realizability models
from specifications.

The interpretation of Krivine realizability in terms of triposes is due to
Streicher [18], and has further been explored in [2]. However, the
presentation here is more straightforward since the constructions and proofs
do not rely on _ordered combinatory algebras_ , but directly rephrase
Krivine’s constructions categorically.

###  5.1 Krivine’s classical realizability

_Throughout this subsection we work with the syntax ( 1) without I/O
instructions but with stack constants._

Krivine’s realizability interpretation is always given relative to a set of
processes called a ‘pole’ – the choice of pole determines the interpretation.

######  Definition 5.1.

A _pole_ is a set
$\Bot\subseteq\mathsf{\mathsf{\Lambda}\\!\star\\!\mathsf{\Pi}}$ of processes
which is _saturated_ , in the sense that $p\in\Bot$ and $p^{\prime}\succ p$
implies $p^{\prime}\in\Bot$.

As Miquel [15] demonstrated, the pole can be seen as playing the role of the
parameter $R$ in Friedman’s negative translation [3]. In the following we
assume that a pole $\Bot$ is fixed.

A _truth value_ is by definition a set $S\subseteq\mathsf{\Pi}$ of stacks.
Given a truth value $S$ and a term $t$, we write $t\real S$ – and say ‘$t$
realizes $S$’ – if $\forall\pi\in S\,.\,t\star\pi\in\Bot$. We write
$S^{\Bot}=\\{t\in\mathsf{\Lambda}\mathrel{|}\,t\real S\\}$ for the set of
realizers of $\mathsf{\Pi}$. So unlike in Kleene realizability the elements of
a truth value are not its realizers – they should rather be seen as
‘refutations’, and indeed larger subsets of $\mathsf{\Pi}$ represent ‘falser’
truth values555For this reason, Miquel [15, 16] calls the elements of
$P(\mathsf{\Pi})$ _falsity values_.; in particular falsity is defined as

$\qquad\bot\quad=\quad\mathsf{\Pi}.$ (14)

Given truth values $S,T\subseteq\mathsf{\Pi}$, we define the implication
$S\Rightarrow T$ as follows.

$S\Rightarrow T\quad=\quad
S^{\Bot}\mathclose{\cdot}T=\\{s\mathclose{\cdot}\pi\mathrel{|}\,s\real
S,\pi\in T\\}$ (15)

With these definitions we can formulate the following lemma, which relates
refutations of a truth value $S$ with realizers of its negation.

######  Lemma 5.2.

Given $\pi\in S\subseteq\mathsf{\Pi}$, we have $\mathsf{k}_{\pi}\real
S\Rightarrow\bot$.

######  Proof 5.3.

We have to show that $\mathsf{k}_{\pi}\star t\mathclose{\cdot}\rho\in\Bot$ for
all $t\real S$ and $\rho\in\mathsf{\Pi}$. This is because
$\mathsf{k}_{\pi}\star t\mathclose{\cdot}\rho\succ t\star\pi$, where $\pi\in
S$ and $t\real S$.

A _(semantic) predicate_ on a set $I$ is a function $\varphi:I\to
P(\mathsf{\Pi})$ from $I$ to truth values. On semantic predicates we define
the basic logical operations of falsity, implication, universal
quantification, and reindexing by

$\begin{array}[]{r@{\quad=\quad}ll}\bot(i)&\mathsf{\Pi}&\text{\it(falsity)}\\\\[2.84526pt]
(\varphi\Rightarrow\psi)(i)&\varphi(i)\Rightarrow\psi(i)=\varphi(i)^{\Bot}\mathclose{\cdot}\psi(i)&\text{\it(implication)}\\\\[2.84526pt]
\forall_{f}(\theta)(i)&\bigcup_{f(j)=i}\theta(j)&\text{\it(universal
quantification)}\\\ f^{*}\varphi&\varphi\circ f&\text{\it(reindexing)}\\\
\end{array}$ (16)

for $\varphi,\psi:I\to P(\mathsf{\Pi})$, $\theta:J\to P(\mathsf{\Pi})$ and
$f:J\to I$. Thus, for any function $f:J\to I$, the function $\forall_{f}$
(called ‘universal quantification along $f$’) maps predicates on $J$ to
predicates on $I$666The usual $\forall x\,\mathclose{:}\,A$ from predicate
logic corresponds to taking $f$ to be a projection map $\pi_{1}:\Gamma\times
A\to\Gamma$, see e.g. [8, Chapter 4]., and the function $f^{*}$ (called
‘reindexing along $f$’) maps predicates on $I$ to predicate on $J$. We write
$\forall_{I}$ for universal quantification along the terminal projection $I\to
1$.

Next, we come to the concept of ‘truth/validity’ of the interpretation. We can
not simply call a truth value ‘true’ if it has a realizer – this would lead to
inconsistency as soon as the pole $\Bot$ is nonempty, since
$\mathsf{k}_{\pi}t\real\bot$ for any process $t\star\pi\in\Bot$. The solution
is to single out a set $\mathsf{PL}$ of ‘well-behaved’ realizers called
‘proof-like terms’. We recall the definition from [10].

######  Definition 5.4.

The set $\mathsf{PL}\subseteq\mathsf{\Lambda}$ of _proof-like terms_ is the
set of terms $t$ that do not contain any continuations $\mathsf{k}_{\pi}$.

As Krivine [10, pg. 2] points out, $t$ is a proof-like term if and only if it
does not contain any stack constant $\pi_{0}\in\mathsf{\Pi}_{0}$ (since
continuation terms $\mathsf{k}_{\pi}$ necessarily contain a stack constant at
the end of $\pi$, and conversely stacks can only occur as continuations in a
term).

Proof-like terms give us a concept of logical validity – a truth value $S$ is
called _valid_ , if there exists a proof-like term $t$ with $t\real S$.

With this notion, we are ready to define the centerpiece of the realizability
model, which is the _entailment relation_ on predicates.

######  Definition 5.5.

For any set $I$ and integer $n$, the $(n+1)$-ary entailment relation
$(\vdash_{I})$ on predicates on $I$ is defined by

$\varphi_{1}\dots\varphi_{n}\vdash_{I}\psi\quad\text{if and only
if}\quad\exists
t\in\mathsf{PL}\,.\,t\real\forall_{I}(\varphi_{1}\Rightarrow\dots\Rightarrow\varphi_{n}\Rightarrow\psi).$

If the right hand side proposition holds, we call $t$ a _realizer_ of
$\varphi_{1}\dots\varphi_{n}\vdash_{I}\psi$.

Thus, $\varphi_{1}\dots\varphi_{n}\vdash_{I}\psi$ means that the truth value
$\forall_{I}(\varphi_{1}\Rightarrow\dots\Rightarrow\varphi_{n}\Rightarrow\psi)$
is valid. More explicitly this can be written out as

$\exists t\in\mathsf{PL}\;\forall i\in
I,u_{1}\in\varphi_{1}(i)^{\Bot},\dots,u_{n}\in\varphi_{n}(i)^{\Bot},\pi\in\psi(i)\,.\,t\star
u_{1}\mathclose{\cdot}\dots\mathclose{\cdot}u_{n}\mathclose{\cdot}\pi\in\Bot.$
(17)

With the aim to show that the semantic predicates form a tripos in Theorem
5.13, we now prove that the entailment ordering models the logical rules in
Table (1). The first eight rules form a standard natural deduction system for
(the $\bot,\Rightarrow$ fragment of) classical propositional logic, but for
universal quantification we give categorically inspired rules that bring us
quicker to where we want, and in particular avoid having to deal with
variables.

(Ax) $\varphi\vdash_{I}\varphi$ $\Gamma\vdash_{I}\bot$ ($\bot$E)
$\Gamma\vdash_{I}\psi$ $\Gamma,\varphi\vdash_{I}\psi$ ($\Rightarrow$I)
$\Gamma\vdash_{I}\varphi\Rightarrow\psi$ $\Gamma\vdash_{I}\psi$
$\Delta\vdash_{I}\psi\Rightarrow\theta$ ($\Rightarrow$E)
$\Gamma,\Delta\vdash_{I}\theta$ $\Gamma\vdash_{I}\psi$ (S)
$\sigma(\Gamma)\vdash_{I}\psi$ (PeL)
$\Delta\mathrel{|}\,\Gamma\vdash_{I}((\psi\Rightarrow\bot)\Rightarrow\psi)\Rightarrow\psi$
$\Gamma\vdash_{I}\psi$ (W) $A,\Gamma\vdash_{I}\psi$ $A,A,\Gamma\vdash_{I}\psi$
(C) $A,\Gamma\vdash_{I}\psi$ $f^{*}\Gamma\vdash_{J}\xi$ ($\forall$I)
$\Gamma\vdash_{I}\forall_{f}\xi$ $\Gamma\vdash_{I}\forall_{f}\xi$ ($\forall$E)
$f^{*}\Gamma\vdash_{J}\xi$ $\varphi,\psi,\theta$ are predicates on $I$, i.e.
functions $I\to P(\mathsf{\Pi})$, and
$\Gamma\equiv\varphi_{1}\dots\varphi_{n}$ and
$\Delta\equiv\psi_{1}\dots\psi_{m}$ are lists of such predicates. $\xi$ is a
predicate on $J$, and $f:J\to I$ is a function. $\sigma$ is a permutation of
$\\{1,\dots,n\\}$. $f^{*}\Gamma$ is an abbreviation for $f^{*}\varphi_{1}\dots
f^{*}\varphi_{n}$, and $\sigma(\Gamma)$ is an abbreviation for
$\varphi_{\sigma(1)}\dots\varphi_{\sigma(n)}$.

Table 1: Admissible rules for the entailment relation.

######  Lemma 5.6.

The rules displayed in Table 1 are admissible for the entailment relation, in
the sense that if the hypotheses hold then so does the conclusion.

######  Proof 5.7.

(Ax) rule: The conclusion is realized by $\lambda x\,.\,x$.

($\bot$E) rule: every realizer of the hypothesis is also a realizer of the
conclusion, since $\psi(i)\subseteq\bot(i)=\mathsf{\Pi}$ for all $i\in I$.

($\Rightarrow$I) rule: the hypothesis and the conclusion have precisely the
same realizers.

($\Rightarrow$E) rule: if $t$ realizes $\Delta\vdash_{I}\psi\Rightarrow\theta$
and $u$ realizes $\Gamma\vdash_{i}\psi$ then $\Gamma,\Delta\vdash_{i}\theta$
is realized by $\lambda x_{1}\dots x_{n}y_{1}\dots y_{m}\,.\,ty_{1}\dots
y_{m}(ux_{1}\dots x_{n})$.

(PeL) rule (‘Peirce’s law’): the conclusion is realized by $\mathsf{c\\!c}$.
To see this, let $i\in I$, $t\real(\psi(i)\Rightarrow\bot)\Rightarrow\psi(i)$,
and $\pi\in\psi(i)$. Then we have $\mathsf{c\\!c}\star
t\mathclose{\cdot}\pi\succ t\star\mathsf{k}_{\pi}\mathclose{\cdot}\pi$, which
is in $\Bot$ since
$\mathsf{k}_{\pi}\mathclose{\cdot}\pi\in(\psi(i)\Rightarrow\bot)\Rightarrow\psi(i)$
by Lemma 5.2 and the definition (16) of implication.

(W) rule: if $t$ realizes $\Gamma\vdash_{I}\psi$, then $\lambda x\,.\,t$
realizes $A,\Gamma\vdash_{I}\psi$.

(C) rule: if $t$ realizes $A,A,\Gamma\vdash_{I}\psi$, then $\lambda x\,.\,txx$
realizes $A,\Gamma\vdash_{I}\psi$.

(S) rule: if $t$ realizes $\Gamma\vdash_{I}\psi$, then $\lambda
x_{\sigma(1)}\dots x_{\sigma(n)}\,.\,tx_{1}\dots x_{n}$ realizes
$\sigma(\Gamma)\vdash_{I}\psi$.

($\forall$I) and ($\forall$E) rules: $\Gamma\vdash_{I}\forall_{f}\xi$ and
$f^{*}\Gamma\vdash_{J}\xi$ have exactly the same realizers. Indeed, a realizer
of $f^{*}\Gamma\vdash_{J}\xi$ is a term $t$ satisfying

$\;\forall j\in
J,u_{1}\in\varphi_{1}(f(j))^{\Bot},\dots,u_{n}\in\varphi_{n}(f(j))^{\Bot},\pi\in\xi(j)\,.\,t\star
u_{1}\mathclose{\cdot}\dots\mathclose{\cdot}u_{n}\mathclose{\cdot}\pi\in\Bot,$

and a realizer of $\Gamma\vdash_{J}\forall_{f}\xi$ is a term $t$ satisfying

$\textstyle\;\forall i\in
I,u_{1}\in\varphi_{1}(i)^{\Bot},\dots,u_{n}\in\varphi_{n}(i)^{\Bot},\pi\in\bigcup_{f(j)=i}\xi(j)\,.\,t\star
u_{1}\mathclose{\cdot}\dots\mathclose{\cdot}u_{n}\mathclose{\cdot}\pi\in\Bot,$

and both statements can be rephrased as a quantification over pairs $(i,j)$
with $f(j)=i$.

We only defined the propositional connectives $\bot,\Rightarrow$, since
$\top,\wedge,\vee,\neg$ can be encoded as follows:

$\begin{array}[]{r@{\defcon}l@{\qquad}r@{\defcon}l@{\qquad}r@{\defcon}l}\top\quad\equiv\quad&\bot\Rightarrow\bot&\neg\varphi\quad\equiv\quad&\varphi\Rightarrow\bot\\\
\varphi\wedge\psi\quad\equiv\quad&(\varphi\Rightarrow(\psi\Rightarrow\bot))\Rightarrow\bot&\varphi\vee\psi\quad\equiv\quad&(\varphi\Rightarrow\bot)\Rightarrow\psi\\\
\end{array}$ (18)

With these encodings it is routine to show the following.

######  Lemma 5.8.

With the connectives $\top,\wedge,\vee,\neg$ encoded as in (18), the rules of
propositional classical natural deduction (e.g. system Nc in [19, Section
2.1.8]) are derivable from the rules in Table 1.

With this we can show that for any set $I$, the binary part of the entailment
relation makes $P(\mathsf{\Pi})^{I}$ into a _Boolean prealgebra_.

######  Definition 5.9.

A _Boolean prealgebra_ is a preorder $(B,\leq)$ which

  1. 1.

has binary _joins_ and _meets_ – denoted by $x\vee y$ and $x\wedge y$ for
$x,y\in D$,

  2. 2.

has a _least element_ $\bot$ and a _greatest element_ $\top$,

  3. 3.

is _distributive_ in the sense that $x\wedge(y\vee z)\cong(x\wedge
y)\vee(x\wedge z)$ for all $x,y,z\in B$, and

  4. 4.

is _complemented_ , i.e. for every $x\in D$ there exists a $\neg x$ with
$x\wedge\neg x\cong\bot$ and $x\vee\neg x\cong\top$.

######  Lemma 5.10.

Writing $\varphi\leq\psi$ for $\varphi\vdash_{I}\psi$,
$(P(\mathsf{\Pi})^{I},\leq)$ is a Boolean prealgebra.

######  Proof 5.11.

The (Ax) rule implies that $\leq$ is reflexive, and transitivity follows from
the derivation

$\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
49.3611pt\hbox{\vbox{\hbox{\hbox{\hskip
4.0pt\hbox{$\varphi\vdash_{I}\psi$}\hskip 4.0pt}\hbox{\hskip
14.45377pt}\vbox{\hbox{\hskip 6.38887pt\hbox{\hskip
4.0pt\hbox{$\psi\vdash_{I}\theta$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to43.776pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\vdash_{I}\psi\Rightarrow\theta$}\hskip 4.0pt}}}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to91.07527pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 30.02461pt\hbox{\hbox{\hskip
4.0pt\hbox{$\varphi\vdash_{I}\theta$}\hskip
4.0pt}}}}}\ignorespaces.\quad\text{}$

Thus, $\leq$ is a preorder on $P(\mathsf{\Pi})^{I}$.

The joins, meets, complements, and least and greatest element are given by the
corresponding logical operations as defined in (16) and (18).

The required properties all follow from derivability of corresponding
entailments and rules in classical natural deduction – for example,
$\varphi\wedge\psi$ is a binary meet of $\varphi$ and $\psi$ since

$(\ast)\text{ the entailments }\varphi\wedge\psi\vdash_{I}\varphi\text{ and
}\varphi\wedge\psi\vdash_{I}\psi\text{ and the rule
}\,\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
25.44444pt\hbox{\vbox{\hbox{\hbox{\hskip
4.0pt\hbox{$\theta\vdash_{I}\varphi$}\hskip 4.0pt}\hbox{\hskip
14.45377pt}\hbox{\hskip 4.0pt\hbox{$\theta\vdash_{I}\psi$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to76.47807pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 13.91354pt\hbox{\hbox{\hskip
4.0pt\hbox{$\theta\vdash_{I}\varphi\wedge\psi$}\hskip 4.0pt}}}}}\ignorespaces$
(19)

are derivable.

Distributivity follows from derivability of the entailments
$\varphi\wedge(\psi\vee\theta)\vdash_{I}(\varphi\wedge\psi)\vee(\varphi\wedge\theta)$
and
$(\varphi\wedge\psi)\vee(\varphi\wedge\theta)\vdash_{I}\varphi\wedge(\psi\vee\theta).$

We now come to _triposes_ , which are a kind categorical model for higher
order logic. We use a ‘strictified’ version of the original definition [7,
Def. 1.2] since this bypasses some subtleties and is sufficient for our
purposes. Furthermore, we are only interested modeling classical logic here,
and thus can restrict attention to triposes whose fibers are Boolean (instead
of Heyting) prealgebras.

######  Definition 5.12.

A _strict 777‘Strict’ refers to the facts that (i) ${\EuScript{P}}$ is a
_functor_ , not merely a pseudofunctor (ii) the Boolean prealgebra structure
is preserved ‘on the nose’ by the monotone maps ${\EuScript{P}}(f)$ (iii) the
Beck-Chevalley condition is required up to equality, not merely isomorphism,
(iv) we require equality and uniqueness in the last condition. Every strict
tripos is a tripos in the usual sense, and conversely it can be shown that any
tripos is equivalent to a strict one. Boolean tripos_ is a contravariant
functor ${\EuScript{P}}:{\mathbf{Set}}^{\mathsf{op}}\to\mathbf{Ord}$ from the
category of sets to the category of preorders such that

  * •

for every set $I$, the preorder ${\EuScript{P}}(I)$ is a Boolean prealgebra,
and for any function $f:J\to I$, the induced monotone map
${\EuScript{P}}(f):{\EuScript{P}}(I)\to{\EuScript{P}}(J)$ preserves all
Boolean prealgebra structure.

  * •

for any $f:J\to I$, ${\EuScript{P}}(f)$ has left and right
adjoints888‘Adjoint’ in the sense of ‘adjoint functor’, where monotone maps
are viewed as functors between degenerate categories.
$\exists_{f}\dashv{\EuScript{P}}(f)\dashv\forall_{f}$ such that

for any pullback square999The square being a pullback means that $f\circ
p=g\circ q$ and $\forall jk\,.\,f(j)=g(k)\Rightarrow\exists!l\,.\,p(l)=j\wedge
q(l)=k$.
$\textstyle{L\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\scriptstyle{p}$$\textstyle{K\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{J\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{I}$
(20)

we have ${\EuScript{P}}(g)\circ\forall_{f}=\forall_{q}\circ{\EuScript{P}}(p)$
(this is the _Beck-Chevalley condition_), and

  * •

there exists a _generic predicate_ , i.e. a set  and an element
${\mathsf{tr}}\in{\EuScript{P}}($ such that for every set $I$ and
$\varphi\in{\EuScript{P}}(I)$ there exists a unique function $f:I\to$ with
${\EuScript{P}}(f)({\mathsf{tr}})=\varphi$.

The assignment $I\mapsto(P(\mathsf{\Pi})^{I},\leq)$ extends to a functor
${\EuScript{P}}_{\Bot}:{\mathbf{Set}}^{\mathsf{op}}\to\mathbf{Ord}$ by letting
${\EuScript{P}}_{\Bot}(f)=f^{*}$, i.e. mapping every function $f:J\to I$ to
the reindexing function along $f$, which is monotone since every realizer of
$\varphi\vdash_{I}\psi$ is also a realizer of $\varphi\circ
f\vdash_{J}\psi\circ f$.

######  Theorem 5.13.

${\EuScript{P}}_{\Bot}$ is a strict Boolean tripos.

######  Proof 5.14.

We have shown in Lemma 5.10 that the preorders $(P(\mathsf{\Pi})^{I},\leq)$
are Boolean prealgebras. It is immediate from (16) that the reindexing
functions $f^{*}$ preserve $\bot$ and $\Rightarrow$, and the other Boolean
operations are preserved since they are given by encodings.

The identity function $\mathrm{id}:P(\mathsf{\Pi})\to P(\mathsf{\Pi})$ is a
generic predicate for ${\EuScript{P}}_{\Bot}$.

The ($\forall$I) and ($\forall$E) rules together imply that the operation
$\forall_{f}:P(\mathsf{\Pi})^{I}\to P(\mathsf{\Pi})^{J}$ is right adjoint to
$f^{*}$ for any $f:J\to I$. Existential quantification along $f:J\to I$ is
given by $\exists_{f}=\neg\circ\forall_{f}\circ\neg$, which is left adjoint to
$f^{*}$ since

$\neg\forall_{f}\neg\varphi\vdash_{I}\psi\quad\text{iff}\quad\neg\psi\vdash_{I}\forall_{f}\neg\varphi\quad\text{iff}\quad
f^{*}\neg\psi\vdash_{J}\neg\varphi\quad\text{iff}\quad\neg
f^{*}\psi\vdash_{J}\neg\varphi\quad\text{iff}\quad\varphi\vdash_{J}f^{*}\psi$

for all $\varphi:J\to P(\mathsf{\Pi})$ and $\psi:I\to P(\mathsf{\Pi})$.

It remains to verify the Beck-Chevalley condition. Given a square as in (20)
we have

$\textstyle
g^{*}\forall_{f}(\varphi(k))=\bigcup\\{\varphi(j)\mathrel{|}\,f(j)=g(k)\\}\quad\text{and}\quad\forall_{q}(p^{*}(k))=\bigcup\\{\varphi(j)\mathrel{|}\,\exists
l\,.\,pl=j\wedge ql=k\\},$

and the two terms are equal since the square is a pullback.

Thus we obtain a tripos ${\EuScript{P}}_{\Bot}$ _for each pole_ $\Bot$. As
Hyland, Johnstone, and Pitts showed in [7], every tripos ${\EuScript{P}}$
gives rise to a topos ${\mathbf{Set}}[{\EuScript{P}}]$ via the _tripos-to-
topos construction_. Since the fibers of the triposes ${\EuScript{P}}_{\Bot}$
are Boolean prealgebras, the toposes ${\mathbf{Set}}[{\EuScript{P}}_{\Bot}]$
are Boolean as well, which means that their internal logic is classical.

####  5.1.1 Consistency

Triposes of the form ${\EuScript{P}}_{\Bot}$ can be degenerate in two ways: if
$\Bot$ is empty then ${\EuScript{P}}_{\Bot}(I)\simeq(P(I),\subseteq)$ for
every set $I$, and the topos ${\mathbf{Set}}[{\EuScript{P}}_{\Bot}]$ is
equivalent to the category ${\mathbf{Set}}$.

If, in the other extreme, the pole is so big that there exists a proof-like
$t$ realizing $\bot$, i.e. falsity is valid in the model, then we have
${\EuScript{P}}_{\Bot}(I)\simeq 1$ for all $I$ (since $t$ realizes every
entailment $\varphi\vdash_{I}\psi$), and the topos
${\mathbf{Set}}[{\EuScript{P}}_{\Bot}]$ is equivalent to the terminal
category.

By _consistency_ we mean that falsity is _not_ valid, or equivalently that

$\forall t\in\mathsf{PL}\;\exists\pi\in\mathsf{\Pi}\,.\,t\star\pi\not\in\Bot.$
(21)

The ‘canonical’ (according to Krivine [12]) non-trivial consistent pole is the
_thread model_ , which is given by postulating a stack constant $\pi_{t}$ for
each proof-like term $t$, and defining
$\Bot=\\{p\in\mathsf{\mathsf{\Lambda}\\!\star\\!\mathsf{\Pi}}\mathrel{|}\,\neg\exists
t\in\mathsf{PL}\,.\,t\star\pi_{t}\leadsto^{*}p\\}.$ Then the processes
$t\star\pi_{t}$ are not in $\Bot$ for any proof-like $t$, which ensures the
validity of condition (21).

In the next section we show how the presence of side effects allows to define
a variety of new, ‘meaningful’ consistent poles.

###  5.2 Krivine realizability with I/O

The developments of the previous section generalize pretty much directly to
the syntax with I/O. Concretely, we carry over the definitions of _pole_ ,
_truth value_ , _realizer_ , _predicate_ , and of the basic logical operations
$\bot,\Rightarrow,\forall$, by replacing $\mathsf{\Lambda}$ with
$\mathsf{\Lambda}_{e}$, $\mathsf{\Pi}$ with $\mathsf{\Pi}_{e}$, and
$\mathsf{\mathsf{\Lambda}\\!\star\\!\mathsf{\Pi}}$ with $\mathsf{P}$.

We point out that in presence of effects, Definition 5.1 only means that
$\Bot$ is saturated w.r.t.  _effect-free_ evaluation, in contrast to Miquel’s
approach [14] where a pole is a set of (what we call) execution contexts,
closed under the entire execution relation.

The concept of proof-like term deserves some reexamination. It turns out that
the appropriate concept of _proof-like term_ is ‘term not containing any side
effects’. This is consistent with Definition 5.4 if we read ‘free of side
effects’ as ‘free of non-logical constructs’, which are the stack constants in
Krivine’s case. Continuation terms, on the other hand, can be considered
proof-like. We redefine therefore:

######  Definition 5.15.

The set $\mathsf{PL}\subseteq\mathsf{\Lambda}_{e}$ of _proof-like terms_ is
the set of terms not containing any of the constants
$\mathsf{r},\mathsf{w\\!0},\mathsf{w\\!1},\mathsf{end}$.

With this rephrased definition of proof-like term, we can define the
entailment relation on the extended predicates in the same way:

######  Definition 5.16.

For any set $I$ and integer $n$, the $(n+1)$-ary entailment relation
$(\vdash_{I})$ on the set $P(\mathsf{\Pi}_{e})^{I}$ of extended predicates on
$I$ is defined by

$\varphi_{1}\dots\varphi_{n}\vdash_{I}\psi\quad\text{if and only
if}\quad\exists
t\in\mathsf{PL}\,.\,t\real\forall_{I}(\varphi_{1}\Rightarrow\dots\Rightarrow\varphi_{n}\Rightarrow\psi).$

As a special case, the ordering on extended predicates is defined by

$\varphi\leq\psi\quad\text{if and only if}\quad\exists
t\in\mathsf{PL}\,.\,t\real\forall_{I}(\varphi\Rightarrow\psi).$

With these definitions, we can state analogues of Lemma 5.10 and Theorem 5.13:

######  Theorem 5.17.

  * •

For each set $I$, the order $(P(\mathsf{\Pi}_{e})^{I},\leq)$ of extended
predicates is a Boolean prealgebra.

  * •

The assignment $I\mapsto(P(\mathsf{\Pi}_{e})^{I},\leq)$ gives rise to a strict
Boolean tripos
${\EuScript{P}}_{\Bot}:{\mathbf{Set}}^{\mathsf{op}}\to\mathbf{Ord}$.

######  Proof 5.18.

This follows from the arguments in Section 5.1, since the proofs of Lemmas
5.2,5.6, 5.8,5.10, and of Theorem 5.13 are not obstructed in any way by the
new constants, nor do they rely on stack constants. The redefinition of
‘proof-like term’ does not cause any problems either, since we never relied on
proof-like terms not containing continuation terms.

The above rephrasing of the definition of proof-like term admits an intuitive
reformulation of the consistency criterion (21):

######  Lemma 5.19.

A pole $\Bot$ is consistent if and only if every $p\in\Bot\setminus\\{\top\\}$
contains a non-logical constant, i.e. one of
$\mathsf{r},\mathsf{w\\!0},\mathsf{w\\!1},\mathsf{end}$.

######  Proof 5.20.

If every element of $p\in\Bot\setminus\\{\top\\}$ contains a non-logical
constant, then $t\star\varepsilon$ is not in $\Bot$ for any proof-like $t$,
which implies (21).

On the other hand, if $t\ast\pi\in\Bot$ does not contain any non-logical
constant then $\mathsf{k}_{\pi}t$ is a proof-like term which realizes $\bot$,
since for any $\rho\in\mathsf{\Pi}_{e}$ we have
$\mathsf{k}_{\pi}t\star\rho\succ\mathsf{k}_{\pi}\star
t\mathclose{\cdot}\rho\succ t\ast\pi\in\Bot$.

####  5.2.1 Poles from specifications

The connection between poles and specifications is established by the
following lemma.

######  Lemma 5.21.

Every set $\Bot$ of processes that is closed under weak bisimilarity is a
pole.

######  Proof 5.22.

This is because $p\approx q$ whenever $p\succ q$, which follows from Lemma
3.5.

Since we can assume that for any reasonable specification the processes
implementing it are closed under weak bisimilarity, we can thus conclude that
for any specification, the set of processes implementing it is a pole. For
example:

  * •

$\Bot_{\mathrm{cp}}$ is the set of processes that read the input, copy every
bit immediately to the output, and terminate when the input is empty. We have
$Y\star(\lambda
x\,.\,\mathsf{r}(\mathsf{w\\!0}\,x)(\mathsf{w\\!1}\,x)\mathsf{end})\in\Bot_{\mathrm{cp}}$.

  * •

$\Bot_{\mathrm{cp^{\prime}}}$ contains the processes that first read the
entire input, and then write out the same string and terminate. We have
$R\star
F\mathclose{\cdot}W\mathclose{\cdot}\overline{0}\in\Bot_{\mathrm{cp^{\prime}}}$
with the notations of Section 4.

  * •

For any partial function $f:\mathbb{N}\rightharpoonup\mathbb{N}$, the pole
$\Bot_{f}$ consists of those processes that implement $f$ in the sense of
Definition 2.1.

  * •

Since poles are closed under unions, we can define the pole
$\Bot_{F}=\bigcup_{f\in F}\Bot_{f}$ for any set
$F\subseteq(\mathbb{N}\rightharpoonup\mathbb{N})$ of partial functions.

####  5.2.2 Toposes from computable functions

We are particularly interested in the poles $\Bot_{f}$ associated to
computable functions $f$, and we want to use the associated triposes
${\EuScript{P}}_{f}={\EuScript{P}}_{\Bot_{f}}$ and toposes
${\mathbf{Set}}[{\EuScript{P}}_{f}]$ to study these functions.

The following theorem provides a first ‘sanity check’, in showing that the
associated models are non-degenerate.

######  Theorem 5.23.

Let $f:\mathbb{N}\rightharpoonup\mathbb{N}$.

  * •

$\Bot_{f}$ is consistent if and only if $f$ is not totally undefined.

  * •

$\Bot_{f}$ is non-empty if and only if $f$ is computable.

######  Proof 5.24.

The first claim follows from Lemma 5.19. If $n\in\mathrm{dom}(f)$ and
$t\star\pi$ implements $f$, then $(t\star\pi,\mathrm{bin}(n),\varepsilon)$
must terminate and thus $t\star\pi$ must contain an $\mathsf{end}$
instruction. The totally undefined function, on the other hand, is by
definition implemented by every process.

For the second claim, we have shown in Theorem 4.8 that every computable $f$
is implemented by some process. Conversely, every implementable function is
computable since the Krivine machine with I/O is an effective model of
computation.

###  5.3 Discussion and future work

The structure and properties of the toposes
${\mathbf{Set}}[{\EuScript{P}}_{f}]$ remain mysterious for the moment, and in
future work we want to explore which kind of properties of $f$ are reflected
in ${\mathbf{Set}}[{\EuScript{P}}_{f}]$. In the spirit of Grothendieck [4] we
want to view the toposes ${\mathbf{Set}}[{\EuScript{P}}_{f}]$ as _geometric_
rather than logical objects, the guiding intuition being that
${\mathbf{Set}}[{\EuScript{P}}_{f}]$ can be seen as representation of _‘the
space of solutions to the algorithmic problem of computing $f$’_, encoding
e.g. information on how algorithms computing $f$ can be decomposed into
simpler parts.

Evident problems to investigate are to understand the lattice of truth values
in ${\mathbf{Set}}[{\EuScript{P}}_{f}]$, and to determine for which pairs
$f,g$ of functions the associated toposes are equivalent, and which functions
can be separated.

A more audacious goal is to explore whether
${\mathbf{Set}}[{\EuScript{P}}_{f}]$ can teach us something about the
complexity of a computable function $f$. The Krivine machine with I/O seems to
be a model of computation that is fine grained enough to recognize and
differentiate time complexity of different implementations of $f$, but it
remains to be seen in how far this information is reflected in the ‘geometry’
of ${\mathbf{Set}}[{\EuScript{P}}_{f}]$.

### Acknowledgements

Thanks to Jakob Grue Simonsen and Thomas Streicher for many discussions.

## References

  * [1] H.P. Barendregt.  The lambda calculus, Its syntax and semantics, volume 103 of Studies in Logic and the Foundations of Mathematics.  North-Holland Publishing Co., Amsterdam, revised edition, 1984.
  * [2] W. Ferrer, J. Frey, M. Guillermo, O. Malherbe, and A. Miquel.  Ordered combinatory algebras and realizability.  arXiv preprint arXiv:1410.5034, 2014.
  * [3] H. Friedman.  Classically and intuitionistically provably recursive functions.  In Higher set theory (Proc. Conf., Math. Forschungsinst., Oberwolfach, 1977), volume 669 of Lecture Notes in Math., pages 21–27. Springer, Berlin, 1978.
  * [4] A. Grothendieck, M. Artin, and J.L. Verdier.  Théorie des topos et cohomologie étale des schémas.  Lecture Notes in Mathematics, 269, 1972.
  * [5] J. Roger Hindley and Jonathan P. Seldin.  Lambda-calculus and combinators, an introduction.  Cambridge University Press, Cambridge, 2008.
  * [6] J.M.E. Hyland.  The effective topos.  In The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Foundations Math., pages 165–216. North-Holland, Amsterdam, 1982.
  * [7] J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts.  Tripos theory.  Math. Proc. Cambridge Philos. Soc., 88(2):205–231, 1980.
  * [8] B. Jacobs.  Categorical logic and type theory.  Elsevier Science Ltd, 2001.
  * [9] J.L. Krivine.  Lambda-calcul, évaluation paresseuse et mise en mémoire.  RAIRO Inform. Théor. Appl., 25(1):67–84, 1991.
  * [10] J.L. Krivine.  Realizability in classical logic.  Panoramas et synthèses, 27:197–229, 2009.
  * [11] J.L. Krivine.  Realizability algebras: a program to well order $\mathbb{R}$.  Log. Methods Comput. Sci., 7(3):3:02, 47, 2011.
  * [12] J.L. Krivine.  Realizability algebras II: New models of $\mathrm{ZF}+\mathrm{DC}$.  Log. Methods Comput. Sci., 8(1):1:10, 28, 2012.
  * [13] R. Milner.  Operational and algebraic semantics of concurrent processes.  In Handbook of theoretical computer science, Vol. B, pages 1201–1242. Elsevier, Amsterdam, 1990.
  * [14] A. Miquel.  Classical modal realizability and side effects.  preprint, 2009.
  * [15] A. Miquel.  Existential witness extraction in classical realizability and via a negative translation.  Log. Methods Comput. Sci., 7(2):2:2, 47, 2011.
  * [16] A. Miquel.  Forcing as a program transformation.  In 26th Annual IEEE Symposium on Logic in Computer Science—LICS 2011, pages 197–206. IEEE Computer Soc., Los Alamitos, CA, 2011.
  * [17] W.P. Stekelenburg.  Realizability Categories.  PhD thesis, Utrecht University, 2013.
  * [18] T. Streicher.  Krivine’s classical realisability from a categorical perspective.  Mathematical Structures in Computer Science, 23(06):1234–1256, 2013\.
  * [19] A.S. Troelstra and H. Schwichtenberg.  Basic proof theory, volume 43 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, Cambridge, 1996.
  * [20] J. van Oosten.  _Classical Realizability_.  Invited talk at “Cambridge Category Theory Seminar”, slides at http://www.staff.science.uu.nl/~ooste110/talks/cambr060312.pdf.
  * [21] J. van Oosten.  Realizability: An Introduction to its Categorical Side.  Elsevier Science Ltd, 2008.