3 Search Results for "Schröder, Matthias"

Document
DOI: 10.4230/LIPIcs.ITP.2019.28
Quantitative Continuity and Computable Analysis in Coq

Authors: Florian Steinberg, Laurent Théry, and Holger Thies

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the results of this paper extend the library. While full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The paper includes a brief description of the most important concepts of Incone and its sub libraries mf and Metric. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that the countably infinite product of a space with itself is isomorphic to a space of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also describe many non-computational results that support the correctness of definitions from the library. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers.
Cite as

Florian Steinberg, Laurent Théry, and Holger Thies. Quantitative Continuity and Computable Analysis in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{steinberg_et_al:LIPIcs.ITP.2019.28,
  author =	{Steinberg, Florian and Th\'{e}ry, Laurent and Thies, Holger},
  title =	{{Quantitative Continuity and Computable Analysis in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.28},
  URN =		{urn:nbn:de:0030-drops-110830},
  doi =		{10.4230/LIPIcs.ITP.2019.28},
  annote =	{Keywords: computable analysis, Coq, contionuous functionals, discontinuity, closed choice on the naturals}
}
Document
Extended Abstract
DOI: 10.4230/OASIcs.CCA.2009.2274
A Note on Closed Subsets in Quasi-zero-dimensional Qcb-spaces (Extended Abstract)

Authors: Matthias Schröder

Published in: OASIcs, Volume 11, 6th International Conference on Computability and Complexity in Analysis (CCA'09) (2009)

Abstract
We introduce the notion of quasi-zero-dimensionality as a substitute for the notion of zero-dimensionality, motivated by the fact that the latter behaves badly in the realm of qcb-spaces. We prove that the category $\QZ$ of quasi-zero-dimensional qcb$_0$-spaces is cartesian closed. Prominent examples of spaces in $\QZ$ are the spaces in the sequential hierarchy of the Kleene-Kreisel continuous functionals. Moreover, we characterise some types of closed subsets of $\QZ$-spaces in terms of their ability to allow extendability of continuous functions. These results are related to an open problem in Computable Analysis.
Cite as

Matthias Schröder. A Note on Closed Subsets in Quasi-zero-dimensional Qcb-spaces (Extended Abstract). In 6th International Conference on Computability and Complexity in Analysis (CCA'09). Open Access Series in Informatics (OASIcs), Volume 11, pp. 233-244, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{schroder:OASIcs.CCA.2009.2274,
  author =	{Schr\"{o}der, Matthias},
  title =	{{A Note on Closed Subsets in Quasi-zero-dimensional Qcb-spaces}},
  booktitle =	{6th International Conference on Computability and Complexity in Analysis (CCA'09)},
  pages =	{233--244},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-12-5},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{11},
  editor =	{Bauer, Andrej and Hertling, Peter and Ko, Ker-I},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.CCA.2009.2274},
  URN =		{urn:nbn:de:0030-drops-22748},
  doi =		{10.4230/OASIcs.CCA.2009.2274},
  annote =	{Keywords: Computable analysis, Qcb-spaces, extendability}
}
Document
DOI: 10.4230/DagSemProc.06341.2
A convenient category of domains

Authors: Ingo Battenfeld, Matthias Schröder, and Alex Simpson

Published in: Dagstuhl Seminar Proceedings, Volume 6341, Computational Structures for Modelling Space, Time and Causality (2007)

Abstract
We motivate and define a category of "topological domains", whose objects are certain topological spaces, generalising the usual $omega$-continuous dcppos of domain theory. Our category supports all the standard constructions of domain theory, including the solution of recursive domain equations. It also supports the construction of free algebras for (in)equational theories, provides a model of parametric polymorphism, and can be used as the basis for a theory of computability. This answers a question of Gordon Plotkin, who asked whether it was possible to construct a category of domains combining such properties.
Cite as

Ingo Battenfeld, Matthias Schröder, and Alex Simpson. A convenient category of domains. In Computational Structures for Modelling Space, Time and Causality. Dagstuhl Seminar Proceedings, Volume 6341, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{battenfeld_et_al:DagSemProc.06341.2,
  author =	{Battenfeld, Ingo and Schr\"{o}der, Matthias and Simpson, Alex},
  title =	{{A convenient category of domains}},
  booktitle =	{Computational Structures for Modelling Space, Time and Causality},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6341},
  editor =	{Ralph Kopperman and Prakash Panangaden and Michael B. Smyth and Dieter Spreen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06341.2},
  URN =		{urn:nbn:de:0030-drops-8945},
  doi =		{10.4230/DagSemProc.06341.2},
  annote =	{Keywords: Domain theory, topology of datatypes}
}
  • Refine by Author
  • 2 Schröder, Matthias
  • 1 Battenfeld, Ingo
  • 1 Simpson, Alex
  • 1 Steinberg, Florian
  • 1 Thies, Holger
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Continuous functions
  • 1 Software and its engineering → Formal methods
  • 1 Theory of computation → Models of computation

  • Refine by Keyword
  • 1 Computable analysis
  • 1 Coq
  • 1 Domain theory
  • 1 Qcb-spaces
  • 1 closed choice on the naturals
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2007
  • 1 2009
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact