一句话：为半直觉主义非标准算术提出带状态 λ-演算的可实现性解释，并给出 Idealization 与 LLPO 的非平凡 realizer。
本文为（半）直觉主义框架下的非标准算术提出新的可实现性解释。作者聚焦用超幂构造非标准模型的 Lightstone–Robinson 方法，将 λ-演算扩展为带整数状态记忆单元的计算系统：该状态指示当前计算位于超幂 M^N 的哪一切片。在此设定下，论文考察可获得的非标准原则及其计算内容，给出 Idealization 和非标准版 LLPO 的非平凡 realizer。最后讨论如何对超幂乘积作商，以模拟 Lightstone–Robinson 构造，把可实现性解释与非标准模型语义联系起来。
In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of (semi)intuitionistic realizability, focusing on the Lightstone-Robinson construction of a model for nonstandard analysis through an ultrapower. In particular, we consider an extension of the $\lambda$-calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower $\cal{M}^{\mathbb{N}}$ the computation is being done. We pay attention to the nonstandard principles (and their computational content) obtainable in this setting. In particular, we give non-trivial realizers to Idealization and a non-standard version of the LLPO principle. We then discuss how to quotient this product to mimic the Lightstone-Robinson construction.