Axiomatic Reals and Certified Efficient Exact Real Computation

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.

Publication DOI: https://doi.org/10.1007/978-3-030-88853-4_16
Divisions: College of Engineering & Physical Sciences > School of Informatics and Digital Engineering > Computer Science
College of Engineering & Physical Sciences
Additional Information: © Springer Nature B.V. 2021. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-88853-4_16 Funding Information: Holger Thies is supported by JSPS KAKENHI Grant Number JP20K19744. Sewon Park is supported by the National Research Foundation of Korea (NRF) grants funded by the Korea government (No. NRF-2016K1A3A7A03950702, NRF-2017R1E1A1A03071032 (MSIT) & No. NRF-2017R1D1A1B05031658 (MOE)).
Event Title: 27th International Workshop, WoLLIC 2021
Event Type: Other
Event Dates: 2021-10-05 - 2021-10-08
Uncontrolled Keywords: Constructive real numbers,Exact real number computation,Formal proofs,Program extraction,Theoretical Computer Science,Computer Science(all)
ISBN: 978-3-030-88852-7
Full Text Link:
Related URLs: https://www.spr ... k/9783030888527 (Publisher URL)
http://www.scop ... tnerID=8YFLogxK (Scopus URL)
PURE Output Type: Conference contribution
Published Date: 2021-11-17
Published Online Date: 2021-10-06
Accepted Date: 2021
Authors: Konečný, Michal (ORCID Profile 0000-0003-2374-9017)
Park, Sewon
Thies, Holger

Download

[img]

Version: Accepted Version

Access Restriction: Restricted to Repository staff only until 6 October 2022.


Export / Share Citation


Statistics

Additional statistics for this record