We apply to the semantics of Arithmetic the idea of ``finite approximation'' used to provide computational interpretations of Herbrand's Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for $\vee, \exists$) over a suitable structure $\StructureN$ for the language of natural numbers and maps of Gödel's system $\SystemT$. We introduce a new Realizability semantics we call ``Interactive learning-based Realizability'', for Heyting Arithmetic plus $\EM_1$ (Excluded middle axiom restricted to $Σ^0_1$ formulas). Individuals of $\StructureN$ evolve with time, and realizers may ``interact'' with them, by influencing their evolution. We build our semantics over Avigad's fixed point result, but the same semantics may be defined over different constructive interpretations of classical arithmetic (Berardi and de' Liguoro use continuations). Our notion of realizability extends intuitionistic realizability and differs from it only in the atomic case: we interpret atomic realizers as ``learning agents''.
Interactive Realizability, Monads and Witness Extraction
在这篇论文中，我们收集了一些关于“交互式可实现性”的结果，可实现性语义扩展的布劳威尔-海廷-柯尔莫戈罗夫解释（子）经典逻辑，更确切地说，一阶直觉算术（海廷算术，HA）扩展的法律的排除中间限制简单的存在公式公式（EM 1），一个系统的动机是其利益证明挖掘。我们描述了一个经典的证明涉及实数的交互式解释。我们证明的陈述是关于实平面上的点的一个简单但非平凡的事实。证明使用EM 1来推导实数上的排序的性质，这是不可判定的，因此从构造性的角度来看是有问题的。我们提出了一组新的自然演绎推导约简，可以从HA + EM 1中简单存在公式的封闭推导中提取证人。我们提出的约简的灵感来自于通过提出可证伪的假设并检查它们来学习的非正式思想，以及交互式的可实现性解释。我们提取证人直接从推导HA + EM 1减少，没有编码推导的可实现性解释。我们给出了一个新的介绍互动的可实现性与更明确的语法。我们表示交互式的实现者通过一个抽象的框架，适用于一元的方法在函数编程修改的可实现性，以获得不太严格的概念，可实现性是适合于经典逻辑。特别是，我们使用状态和异常单子的组合，以捕捉从错误中学习的交互式实现器的性质。
A Witness Extraction Technique by Proof Normalization Based on Interactive Realizability
我们提出了一套新的减少自然演绎推导，可以提取证人从封闭的推导简单的存在公式在海廷算术（HA）加上排除中间法限制简单的存在公式（EM 1），一个系统的动机是其利益证明挖掘。我们对经典逻辑的归约与所有现有的归约都大不相同。他们的灵感来自于通过提出可证伪的假设并检验它们来学习的非正式思想，以及交互式的可实现性解释。我们提取证人直接从推导HA+ EM 1减少，没有编码推导的可实现性解释。
Realizability Interpretation and Normalization of Typed Call-by-Need $$λ$$-calculus With Control
我们定义了一个变体的可实现性，其中实现者是一个长期和一个替代对。这个变体允许我们证明一个简单类型的按需调用$$λ$-$calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need $$ λ$-演算的规范化，该演算配备了一个等价于经典二阶谓词逻辑的类型系统，代表了向证明按需调用经典二阶算术的规范化迈出的一步，该算术由第二作者引入，以提供依赖选择公理的证明即程序解释。
Gödel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication
School of Computing The Australian National University（澳大利亚国立大学计算机学院）；Chair For Theoretical Computer Science FAU Erlangen-Nuremberg（埃尔朗根-纽伦堡大学理论计算机科学教席）
Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability
IIT Bombay（印度理工学院孟买分校）；The Institute of Mathematical Sciences, Chennai（金奈数学科学研究所）；Homi Bhabha National Institute（霍米·巴巴国立研究所）；University of California at Berkeley（加州大学伯克利分校）
