Certified Computation of Nondeterministic Limits

Michal Konečný, Sewon Park, Holger Thies

Research output: Chapter in Book/Published conference outputConference publication


The computational content of constructive metric completeness is the operator that computes limits of Cauchy sequences. It can be used to construct certified programs that compute interesting transcendental real numbers from sequences of approximations. The desired nondeterministic version of it would be to nondeterministically compute real numbers from nondeterministic approximations. However, it is not obvious how nondeterministic metric completeness should be formalized.

We extend previous work on the formalization of exact real computation by primitive properties of nondeterminism. We show that by these properties, various forms of nondeterministic metric completeness can be derived without extending the axiomatic structure of constructive real numbers. We further implement our theory in the Coq proof assistant and use Coq’s code extraction features to extract efficient exact real computation programs using several forms of nondeterministic computation.
Original languageEnglish
Title of host publicationNASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings
Subtitle of host publication14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings
EditorsJyotirmoy V. Deshmukh, Klaus Havelund, Ivan Perez
Number of pages19
ISBN (Electronic)978-3-031-06773-0
ISBN (Print)978-3-031-06772-3
Publication statusPublished - 20 May 2022

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • Constructive real numbers
  • Exact real number computation
  • Formal proofs
  • Nondeterminism
  • Program extraction


Dive into the research topics of 'Certified Computation of Nondeterministic Limits'. Together they form a unique fingerprint.

Cite this