Axiomatic Reals and Certified Efficient Exact Real Computation

Michal Konečný, Sewon Park, Holger Thies

Research output: Chapter in Book/Published conference outputConference publication

Abstract

We introduce a new axiomatization of the constructive real numbers in a dependent type theory.
Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs.
We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis.
We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive.
We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples.
From the examples we can automatically extract Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers.
In experiments, the extracted programs behave similarly to native implementations in AERN in terms of running time.
Original languageEnglish
Title of host publicationLogic, Language, Information, and Computation
Subtitle of host publication 27th International Workshop, WoLLIC 2021
EditorsAlexandra Silva, Renata Wassermann, Ruy de Queiroz
Place of PublicationBerlin / Heidelberg
PublisherSpringer
Volume13038
ISBN (Print)978-3-030-88852-7
DOIs
Publication statusAccepted/In press - 2021
Event27th International Workshop, WoLLIC 2021 -
Duration: 5 Oct 20218 Oct 2021

Publication series

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

Conference

Conference27th International Workshop, WoLLIC 2021
Period5/10/218/10/21

Keywords

  • Constructive Real Numbers
  • Formal Proofs
  • Exact Real Number Computation
  • Program Extraction.

Fingerprint

Dive into the research topics of 'Axiomatic Reals and Certified Efficient Exact Real Computation'. Together they form a unique fingerprint.

Cite this