2026-07-21T23:54:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13453 2024-03-06T10:52:07Z ddc:004 open_access

Realizability with Stateful Computations for Nonstandard Analysis Dinis, Bruno Miquey, Étienne realizability nonstandard analysis states glueing ultrafilters Łoś' theorem In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of 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 λ-calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower ℳ^{ℕ} the computation is being done. We shall pay attention to the nonstandard principles (and their computational content) obtainable in this setting. We then discuss how this product could be quotiented to mimic the Lightstone-Robinson construction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bruno Dinis and Étienne Miquey 2021 Is Part Of LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2021.19 urn:nbn:de:0030-drops-134531 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.19 eng https://creativecommons.org/licenses/by/3.0/legalcode