This dissertation concerns the computational interpretation of analysis via proof
interpretations, and examines the variants of bar recursion that have been used to interpret …

In [45] and again in [46] Georg Kreisel reflected at length on Church's Thesis CT, the
principle formulated in 1936 by Alonzo Church ([10]) as a definition:“We now define the …

We show that it is possible to define a realizability interpretation for the $\Sigma_2 $-
fragment of classical Analysis using G\" odel's System T only. This supplements a previous …

In this chapter, we propose some future directions of work, potentially beneficial to
Mathematics and its foundations, based on the recent import of methodology from the theory …

We consider the Double-negation Shift (DNS) as a constructive principle in its own right and
its effect on modified realizability (MR) and Dialectica (D) interpretations. We notice that DNS …

Hilbert's Program had as the goal to interpret all ideal principles used in mathematical proofs
by elementary notions. While Gödel's Incompleteness theorems showed that those notions …

In the view of recent works on constructive interpretations of MP and DNS using delimited
control operators [2, 3], we reconstruct a direct proof of Veldman's result that derives OI by …