  In this dissertation we collect some results about "interactive
realizability", a realizability semantics that extends the
Brouwer-Heyting-Kolmogorov interpretation to (sub-)classical logic, more
precisely to first-order intuitionistic arithmetic (Heyting Arithmetic, HA)
extended by the law of the excluded middle restricted to simply existential
formulas formulas (EM1), a system motivated by its interest in proof mining.
  We describe the interactive interpretation of a classical proof involving
real numbers. The statement we prove is a simple but non-trivial fact about
points in the real plane. The proof employs EM1 to deduce properties of the
ordering on the real numbers, which is undecidable and thus problematic from a
constructive point of view.
  We present a new set of reductions for derivations in natural deduction that
can extract witnesses from closed derivations of simply existential formulas in
HA + EM1. The reduction we present are inspired by the informal idea of
learning by making falsifiable hypothesis and checking them, and by the
interactive realizability interpretation. We extract the witnesses directly
from derivations in HA + EM1 by reduction, without encoding derivations by a
realizability interpretation.
  We give a new presentation of interactive realizability with a more explicit
syntax. We express interactive realizers by means of an abstract framework that
applies the monadic approach used in functional programming to modified
realizability, in order to obtain less strict notions of realizability that are
suitable to classical logic. In particular we use a combination of the state
and exception monads in order to capture the learning-from-mistakes nature of
interactive realizers.
