Skip to main content

Axiomatic Reals and Certified Efficient Exact Real Computation

Part of the Lecture Notes in Computer Science book series (LNTCS,volume 13038)


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 hand-written implementations in AERN in terms of running time.


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

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)).

This project has received funding from the EU’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 731143.

This is a preview of subscription content, access via your institution.

Buying options

USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
USD   59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions


  1. 1.

    Assemblies are generalizations of represented sets [13, 25] which are exactly the assemblies where the surjective relations are required to be partial surjective functions. The terminology multi-representation [20] may be more familiar to some readers.

  2. 2.

    However, this is no longer true if we assumed counter-classical axioms such as the continuity principle.

  3. 3.

    The source code is on

  4. 4.

    For sake of presentation, we applied some slight, non-essential simplifications to the Coq statements in this section compared to the original source code.

  5. 5.

    Benchmarks were run 10 times on a Lenovo T440p laptop with Intel i7-4710MQ CPU and 16 GB RAM, OS Ubuntu 18.04, compiled using Haskell Stackage LTS 17.2.


  1. Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.L.: Ariadne: a framework for reachability analysis of hybrid automata. In: Proceedings of the International Symposium on Mathematical Theory of Networks and Systems (2006)

    Google Scholar 

  2. Boldo, S., Filliâtre, J.-C., Melquiond, G.: Combining Coq and Gappa for certifying floating-point programs. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) CICM 2009. LNCS (LNAI), vol. 5625, pp. 59–74. Springer, Heidelberg (2009).

    CrossRef  Google Scholar 

  3. Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196–1233 (2016).

  4. Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: 2011 IEEE 20th Symposium on Computer Arithmetic, pp. 243–252. IEEE (2011)

    Google Scholar 

  5. Brattka, V., Hertling, P.: Feasible real random access machines. J. Complex. 14(4), 490–526 (1998).

  6. Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004).

    CrossRef  Google Scholar 

  7. Hertling, P.: A real number structure that is effectively categorical. Math. Log. Q. 45, 147–182 (1999).

    CrossRef  Google Scholar 

  8. Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 427–441. Springer, Heidelberg (1995).

    CrossRef  Google Scholar 

  9. Kawamura, A., Steinberg, F., Thies, H.: Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving. In: Moss, L.S., de Queiroz, R., Martinez, M. (eds.) WoLLIC 2018. LNCS, vol. 10944, pp. 223–236. Springer, Heidelberg (2018).

    CrossRef  Google Scholar 

  10. Konečný, M.: aern2-real: A Haskell library for exact real number computation (2021).

  11. Konečný, M., Steinberg, F., Thies, H.: Computable analysis for verified exact real computation. In: 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2020)

    Google Scholar 

  12. Koswara, I., Selivanova, S., Ziegler, M.: Computational complexity of real powering and improved solving linear differential equations. In: van Bevern, R., Kucherov, G. (eds.) CSR 2019. LNCS, vol. 11532, pp. 215–227. Springer, Cham (2019).

    CrossRef  Google Scholar 

  13. Kreitz, C., Weihrauch, K.: Theory of representations. Theoret. Comput. Sci. 38, 35–53 (1985)

    CrossRef  Google Scholar 

  14. Luckhardt, H.: A fundamental effect in computations on real numbers. Theoret. Comput. Sci. 5(3), 321 – 324 (1977).

  15. Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 2–17. Springer, Heidelberg (2008).

    CrossRef  Google Scholar 

  16. Müller, N.T.: The iRRAM: exact arithmetic in C++. In: Blanck, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 222–252. Springer, Heidelberg (2001).

    CrossRef  Google Scholar 

  17. Palmgren, E.: On universes in type theory. In: Twenty Five Years of Constructive Type Theory, pp. 191–204 (1998)

    Google Scholar 

  18. Park, S., et al.: Foundation of computer (algebra) analysis systems: semantics, logic, programming, verification. arXiv e-prints arXiv:1608.05787 (2016)

  19. Reus, B.: Realizability models for type theories. Electron. Notes Theoret. Comput. Sci. 23(1), 128–158 (1999)

    CrossRef  Google Scholar 

  20. Schröder, M.: Effectivity in spaces with admissible multirepresentations. Math. Logic Q. 48(S1), 78–90 (2002)

    CrossRef  Google Scholar 

  21. Schwichtenberg, H.: Constructive analysis with witnesses. In: Proof Technology and Computation. Natio Science Series, pp. 323–354 (2006)

    Google Scholar 

  22. Seely, R.A.G.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95(1), 33–48 (1984).

    CrossRef  Google Scholar 

  23. Steinberg, F., Thery, L., Thies, H.: Computable analysis and notions of continuity in Coq. Log. Methods Comput. Sci. 17(2), May 2021.

  24. Van Oosten, J.: Realizability: an introduction to its categorical side. Elsevier (2008)

    Google Scholar 

  25. Weihrauch, K.: Computable Analysis. Springer, Berlin (2000).

    CrossRef  Google Scholar 

Download references

Author information

Authors and Affiliations


Corresponding author

Correspondence to Holger Thies .

Editor information

Editors and Affiliations


A Full List of Axioms

Here we list all our axioms, grouped by the files in our implementation.

Base.v defines our base type theory, making it extensional and \(\mathsf {Prop}\) classical:

  1. TT1

    \(\mathrm {\Pi }( P : \mathsf {Prop}).\ P \vee \lnot P\)

  2. TT2

    \(\mathrm {\Pi }( P,Q: \mathsf {Prop}).\ (P \rightarrow Q) \rightarrow (Q \rightarrow P) \rightarrow P = Q\)

  3. TT3

    \( \mathrm {\Pi }( A : \mathsf {Type}).\ \mathrm {\Pi }( P : A \rightarrow \mathsf {Type}).\ \mathrm {\Pi }( f, g : \mathrm {\Pi }( x : A).\ P(x)).\ (\mathrm {\Pi }( x: A).\ f\, x = g\, x) \rightarrow f = g\)

Kleene.v axiomatizes the type of Kleeneans and the multivalued monad.

  1. K1

    \(\textsf {K}: \mathsf {Type}\)

  2. K2

    \(\textsf {true}: \textsf {K}\)

  3. K3

    \(\textsf {false}: \textsf {K}\)

  4. K4

    \(\textsf {true}\ne \textsf {false}\)

  5. K5

    \(\hat{\lnot }: \textsf {K}\rightarrow \textsf {K}\)

  6. K6

    \(\mathrel {\hat{\vee }}: \textsf {K}\rightarrow \textsf {K}\rightarrow \textsf {K}\)

  7. K7

    \(\mathrel {\hat{\wedge }}: \textsf {K}\rightarrow \textsf {K}\rightarrow \textsf {K}\)

    Define \(\lceil k :\mathsf {K} \rceil :\equiv k = \textsf {true}\), \(\lfloor k : \mathsf {K} \rfloor :\equiv k = \textsf {false}\), and \((k : \mathsf {K}) \!\downarrow :\equiv \lceil k \rceil \vee \lfloor k \rfloor \).

  8. K8

    \(x \!\downarrow \rightarrow \lceil x \rceil + \lfloor x \rfloor \)

    Kleene logic operations:

  9. K9

    \(\lceil \hat{\lnot }x \rceil = \lfloor x \rfloor \) and \(\lfloor \hat{\lnot }x \rfloor = \lceil x \rceil \)

  10. K10

    \(\lceil x \mathrel {\hat{\wedge }}y \rceil = (\lceil x \rceil \wedge \lceil y \rceil )\) and \(\lfloor x \mathrel {\hat{\wedge }}y \rfloor = (\lfloor x \rfloor \vee \lfloor y \rfloor )\)

  11. K11

    \(\lceil x \mathrel {\hat{\vee }}y \rceil = (\lceil x \rceil \vee \lceil y \rceil )\) and \(\lfloor x \mathrel {\hat{\vee }}y \rfloor = (\lfloor x \rfloor \wedge \lfloor y \rfloor )\)

  • The monad structure:

  1. M1

    \(\mathsf {M}: \mathsf {Type}\rightarrow \mathsf {Type}\)

  2. M2

    \(\textsf {unitM}: \mathrm {\Pi }( A : \mathsf {Type}).\ A \rightarrow \mathsf {M}\ A\)

  3. M3

    \(\mathsf {multM}: \mathrm {\Pi }( A : \mathsf {Type}).\ \mathsf {M}\ (\mathsf {M}\ A) \rightarrow \mathsf {M}\ A\)

  4. M4

    \(\mathsf {liftM}: \mathrm {\Pi }( A, B : \mathsf {Type}).\ (A \rightarrow B) \rightarrow (\mathsf {M}\ A \rightarrow \mathsf {M}\ B)\)

    \(\textsf {unitM}\) and \(\mathsf {multM}\) are natural transformations:

  5. M5

    \(\mathrm {\Pi }( A, B : \mathsf {Type}).\ \mathrm {\Pi }( f : A \rightarrow B).\ \mathrm {\Pi }( x : A).\ \mathsf {liftM}\ A\ B\ f(\textsf {unitM}\ A\ x) = \textsf {unitM} B\ (f\ x)\)

  6. M6

    \(\mathrm {\Pi }( A, B : \mathsf {Type}).\ \mathrm {\Pi }( f : A \rightarrow B).\ \mathrm {\Pi }( x : \mathsf {M}\ (\mathsf {M}\ A)).\ \)

    \(\mathsf {multM}\ B ((\mathsf {liftM}\ (\mathsf {M}\ A)\ (\mathsf {M}\ B)\ (\mathsf {liftM}\ A\ B\ f))\ x) = (\mathsf {liftM}\ A\ B\ f) (\mathsf {multM}\ A\ x)\)

    The coherence conditions:

  7. M7

    \(\mathrm {\Pi }( A:\mathsf {Type}).\ \mathrm {\Pi }( x : \mathsf {M}\ A).\ \mathsf {multM}\ A\ (\textsf {unitM}\ (\mathsf {M}\ A)\ x) = x\)

  8. M8

    \(\mathrm {\Pi }( A :\mathsf {Type}).\ \mathrm {\Pi }( x : \mathsf {M}\ A).\ \mathsf {multM}\ A\ (\mathsf {liftM}\ A\ (\mathsf {M}\ A)\ (\textsf {unitM}\ A)\ x) = x\)

  9. M9

    \(\mathrm {\Pi }( A : \mathsf {Type}).\ \mathrm {\Pi }( x : \mathsf {M}\ (\mathsf {M}\ (\mathsf {M}\ A))).\ \mathsf {multM}\ A\ (\mathsf {multM}\ (\mathsf {M}\ A)\ x) =\)

    \(\mathsf {multM}\ A\ (\mathsf {liftM}\ (\mathsf {M}\ (\mathsf {M}\ A)) (\mathsf {M}\ A) (\mathsf {multM}\ A)\ x)\)

    Further characterization of the monad:

  10. M10

    \(\textsf {elimM}:\mathrm {\Pi }( A : \mathsf {Type}).\ (\mathrm {\Pi }( x, y : A).\ x = y) \rightarrow \mathsf {M}\ A \rightarrow A\)

  11. M11

    \( \mathrm {\Pi }( A : \mathsf {Type}).\ \mathrm {\Pi }( p : \big (\mathrm {\Pi }( x, y : A).\ x = y\big )).\ \mathrm {\Pi }( a : \mathsf {M}\, A).\ \textsf {unitM}\, A\, \big ( \textsf {elimM}\, A p\, a\big ) = a \)

  12. M12

    \(\mathsf {\omega lift}: \mathrm {\Pi }( P : \mathsf {N}\rightarrow \mathsf {Type}).\ \big (\mathrm {\Pi }( x : \mathsf {N}).\ \mathsf {M}\ P(x)\big ) \rightarrow \mathsf {M}\big (\mathrm {\Pi }( x : \mathsf {N}).\ P(x)\big )\)

  13. M13

    \( \mathrm {\Pi }( P : \mathsf {N}\rightarrow \mathsf {Type}).\ \mathrm {\Pi }( f : \big (\mathrm {\Pi }( x : \mathsf {N}).\ \mathsf {M}\ P(x)\big )).\ f\ n = \lambda ( n : \mathsf {N} ).\ \mathsf {liftM}\big (\lambda ( f : \big (\mathrm {\Pi }( x : \mathsf {N}).\ P(x)\big ) ).\ f\ n\big )\ (\mathsf {\omega lift}\ P\ f) \)

  14. M14

    \(\textsf {select}: \mathrm {\Pi }( x, y : \mathsf {K}).\ (\lceil x \rceil \vee \lceil y \rceil ) \rightarrow \mathsf {M}\ \big (\lceil x \rceil + \lceil y \rceil \big )\)

RealAxioms.v axiomatizes the real numbers:

  • The structure of real numbers:

  1. R1

    \(\mathsf {R}: \mathsf {Type}\)

  2. R2

    \(0 : \mathsf {R}\)

  3. R3

    \(1 : \mathsf {R}\)

  4. R4

    \(+ : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {R}\)

  5. R5

    \(\times : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {R}\)

  6. R6

    \(- : \mathsf {R}\rightarrow \mathsf {R}\)

  7. R7

    \(/ : \mathrm {\Pi }( x : \mathsf {R}).\ x \ne 0 \rightarrow \mathsf {R}\)

  8. R8

    \(< : \mathsf {R}\rightarrow \mathsf {R}\rightarrow \mathsf {Prop}\)

    Semi-decidability of comparison tests:

  9. R9

    \(\mathrm {\Pi }( x, y : \mathsf {R}).\ \textsf {semiDec}(x < y)\)

    Constructive completeness:

  10. R10

    \( \mathrm {\Pi }( P : \mathsf {R}\rightarrow \mathsf {Prop}).\ (\exists !( x :\mathsf {R} ).\ P\ x) \rightarrow (\mathrm {\Pi }( n :\mathsf {N}).\ \mathrm {\Sigma }( x : \mathsf {R}).\ \exists (\tilde{x} : \mathsf {R} ).\ P\ x \wedge - 2^{-n}< x - \tilde{x} < 2^{-n}) \rightarrow \mathrm {\Sigma }( x : \mathsf {R}).\ P\ x\)

    Classical axioms in \(\mathsf {Prop}\):

  11. R11

    \(\mathrm {\Pi }( x, y:\mathsf {R}).\ x + y = y + x\)

  12. R12

    \(\mathrm {\Pi }( x, y,z:\mathsf {R}).\ (x + y) + z = x + (y + z)\)

  13. R13

    \(\mathrm {\Pi }( x:\mathsf {R}).\ x + - x = 0\)

  14. R14

    \(\mathrm {\Pi }( x:\mathsf {R}).\ 0 + x = x\)

  15. R15

    \(\mathrm {\Pi }( x, y:\mathsf {R}).\ x \times y = y \times x\)

  16. R16

    \(\mathrm {\Pi }( x, y, z : \mathsf {R}).\ (x \times y) \times z = x \times (y \times z)\)

  17. R17

    \(\mathrm {\Pi }( x:\mathsf {R}).\ \mathrm {\Pi }( p : x \ne 0).\ (/\ x\ p) \times x = 1\)

  18. R18

    \(\mathrm {\Pi }( x:\mathsf {R}).\ 1 \times x= x\)

  19. R19

    \( \mathrm {\Pi }( x,y,z:\mathsf {R}).\ x \times (y + z) = x \times y + x \times z\)

  20. R20

    \(1 \ne 0\)

  21. R21

    \(1 > 0\)

  22. R22

    \(\mathrm {\Pi }( x, y :\mathsf {R}).\ x < y \vee x = y \vee x > y\)

  23. R23

    \(\mathrm {\Pi }( x,y : \mathsf {R}).\ x< y \rightarrow \lnot (y < x)\)

  24. R24

    \(\mathrm {\Pi }( x,z,y :\mathsf {R}).\ x< y \rightarrow y< z \rightarrow x < z\)

  25. R25

    \(\mathrm {\Pi }( x, y, z :\mathsf {R}).\ y< z \rightarrow x + y < x + z\)

  26. R26

    \(\mathrm {\Pi }( x, y, z : \mathsf {R}).\ 0< x \rightarrow y< z \rightarrow x\times y < x \times z\)

    Define \(x \le y :\equiv x < y \vee x = y\). For each \(P : \mathsf {R}\rightarrow \mathsf {Prop}\) and \(x : \mathsf {R}\), define \(P < x : \equiv \mathrm {\Pi }( y : \mathsf {R}).\ P\ y \rightarrow y \le x\).

  27. R27

    \(\mathrm {\Pi }( P : \mathsf {R}\rightarrow \mathsf {Prop}).\ (\exists (x : \mathsf {R} ).\ P\ x) \rightarrow (\exists (x : \mathsf {R} ).\ P \le x ) \rightarrow \exists (x : \mathsf {R} ).\ P \le x \wedge \mathrm {\Pi }( y : \mathsf {R}).\ P \le y \rightarrow x \le y\).

Nabla.v defines the idempotent monad \(\nabla \) and RealCoqReal.v axiomatizes the relator:

\(\nabla \)1:

\(\textsf {relator}: \mathsf {R}\rightarrow \nabla \tilde{\mathsf {R}}\)

\(\nabla \)2:

\(\mathrm {\Pi }( x, y :\mathsf {R}).\ \textsf {relator}\ x = \textsf {relator}\ y \rightarrow x = y\)

\(\nabla \)3:

\(\mathrm {\Pi }( y : \nabla \tilde{\mathsf {R}}).\ \exists (x :\mathsf {R} ).\ y = \textsf {relator}\ x\)

\(\nabla \)4:

\(\textsf {relator}\ 0 = \textsf {unit}_{\nabla }\!\ \tilde{\mathsf {R}}\ 0\)

\(\nabla \)5:

\(\textsf {relator}\ 1 = \textsf {unit}_{\nabla }\!\ \tilde{\mathsf {R}}\ 1\)

\(\nabla \)6:

\(\mathrm {\Pi }( x, y : \mathsf {R}).\ \textsf {relator}\ (x + y) = (\textsf {relator}\ x) \mathrel {{+}^{\dagger _{\nabla }}} (\textsf {relator}\ y)\)

\(\nabla \)7:

\(\mathrm {\Pi }( x, y : \mathsf {R}).\ \textsf {relator}\ (x \times y) = (\textsf {relator}\ x) \mathrel {{\times }^{\dagger _{\nabla }}} (\textsf {relator}\ y)\)

\(\nabla \)8:

\(\mathrm {\Pi }( x : \mathsf {R}).\ \textsf {relator}\ (-x) = \mathrel {{-}^{\dagger _{\nabla }}} (\textsf {relator}\ x)\)

\(\nabla \)9:

\(\mathrm {\Pi }( x : \mathsf {R}).\ \mathrm {\Pi }( p : x \ne 0).\ \textsf {relator}\ (/x\ p) = \mathrel {{/}^{\dagger _{\nabla }}} (\textsf {relator}\ x)\)

\(\nabla \)10:

\(\mathrm {\Pi }( x, y : \mathsf {R}).\ (x< y) = (\textsf {relator}\ x) \mathrel {{<}^{\dagger _{\nabla }}} (\textsf {relator}\ y)\)

B Code Extraction

Extraction is defined in file Extract.v, including the following key mappings:

figure ab

Note that the monad \(\mathsf {M}\) does not appear in the extracted programs. Multivaluedness is intrinsic thanks to redundancy in the underlying representations.

The AERN comparison OGB.< returns a (lazy) Kleenean for real numbers.

Running the extracted code requires adding a few import statements, which are specified in file Extract.v.

Rights and permissions

Reprints and Permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Konečný, M., Park, S., Thies, H. (2021). Axiomatic Reals and Certified Efficient Exact Real Computation. In: Silva, A., Wassermann, R., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2021. Lecture Notes in Computer Science(), vol 13038. Springer, Cham.

Download citation

  • DOI:

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-88852-7

  • Online ISBN: 978-3-030-88853-4

  • eBook Packages: Computer ScienceComputer Science (R0)