Creative Commons Attribution 4.0 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: https://drops.dagstuhl.de/opus/volltexte/2023/17476/
Cohen, Liron ; Rahli, Vincent
Realizing Continuity Using Stateful Computations
| pdf-format: |
|
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 | |
| Seminar: | 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 |
