  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.
