DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2021.19

Realizability with Stateful Computations for Nonstandard Analysis

Authors: Bruno Dinis and Étienne Miquey

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

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.

Cite as

Bruno Dinis and Étienne Miquey. Realizability with Stateful Computations for Nonstandard Analysis. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dinis_et_al:LIPIcs.CSL.2021.19,
  author =	{Dinis, Bruno and Miquey, \'{E}tienne},
  title =	{{Realizability with Stateful Computations for Nonstandard Analysis}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{19:1--19:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.19},
  URN =		{urn:nbn:de:0030-drops-134531},
  doi =		{10.4230/LIPIcs.CSL.2021.19},
  annote =	{Keywords: realizability, nonstandard analysis, states, glueing, ultrafilters, {\L}o\'{s}' theorem}
}

Search Results

Documents authored by Dinis, Bruno

Realizability with Stateful Computations for Nonstandard Analysis

Abstract

Cite as

Thanks for your feedback!

Could not send message