License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2023.15
URN: urn:nbn:de:0030-drops-174761
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17476/
Go to the corresponding LIPIcs Volume Portal

Cohen, Liron ; Rahli, Vincent

Realizing Continuity Using Stateful Computations

pdf-format:
LIPIcs-CSL-2023-15.pdf (1 MB)

Abstract

The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as System T. Roughly speaking, it states that functions on real numbers only need approximations of these numbers to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or reference cells. This paper presents a class of intuitionistic theories that features stateful computations, such as reference cells, and shows that these theories can be extended with continuity axioms. The modulus of continuity of the functionals on the Baire space is directly computed using the stateful computations enabled in the theory.

BibTeX - Entry

@InProceedings{cohen_et_al:LIPIcs.CSL.2023.15,
  author =	{Cohen, Liron and Rahli, Vincent},
  title =	{{Realizing Continuity Using Stateful Computations}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17476},
  URN =		{urn:nbn:de:0030-drops-174761},
  doi =		{10.4230/LIPIcs.CSL.2023.15},
  annote =	{Keywords: Continuity, Stateful computations, Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda}
}

Keywords: Continuity, Stateful computations, Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda
Collection: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Issue Date: 2023
Date of publication: 01.02.2023
Supplementary Material: Model (Agda Formalization): https://github.com/vrahli/opentt

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI