{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:42:39Z","timestamp":1767926559737,"version":"3.49.0"},"reference-count":54,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T00:00:00Z","timestamp":1729209600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP20K19744"],"award-info":[{"award-number":["JP20K19744"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP23H03346"],"award-info":[{"award-number":["JP23H03346"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP18H03203"],"award-info":[{"award-number":["JP18H03203"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP22F22071"],"award-info":[{"award-number":["JP22F22071"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,7,29]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus solely on the mathematical properties of the problem without thinking about the subtleties of representing real numbers. We propose a new axiomatization of the real numbers in a dependent type theory with the goal of extracting certified exact real computation programs from constructive proofs. Our formalization differs from similar approaches, in that we formalize the reals in a conceptually similar way as some mature implementations of exact real computation. Primitive operations on reals can be extracted directly to the corresponding operations in such an implementation, producing more efficient programs. We particularly focus on the formalization of partial and nondeterministic computation, which is essential in exact real computation. We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis and show how to relate our theory to a classical formalization of the reals. We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples. From the examples we have automatically extracted 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 and memory usage.<\/jats:p>","DOI":"10.1093\/logcom\/exae066","type":"journal-article","created":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T03:09:26Z","timestamp":1729220966000},"source":"Crossref","is-referenced-by-count":2,"title":["Extracting efficient exact real number computation from proofs in constructive type theory"],"prefix":"10.1093","volume":"35","author":[{"given":"Michal","family":"Kone\u010dn\u00fd","sequence":"first","affiliation":[{"name":"Aston University , College of Engineering and Physical Sciences, Birmingham B4 7ET, UK"}]},{"given":"Sewon","family":"Park","sequence":"additional","affiliation":[{"name":"Kyoto University , Graduate School of Informatics, Kyoto 606-8501,","place":["Japan"]}]},{"given":"Holger","family":"Thies","sequence":"additional","affiliation":[{"name":"Kyoto University , Graduate School of Human and Environmental Studies, Kyoto 606-8501,","place":["Japan"]}]}],"member":"286","published-online":{"date-parts":[[2024,10,18]]},"reference":[{"key":"2025090809272766600_ref1","article-title":"Ariadne: a framework for reachability analysis of hybrid automata","volume-title":"Proceedings of the International Symposium on Mathematical Theory of Networks and Systems","author":"Balluchi","year":"2006"},{"key":"2025090809272766600_ref2","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/s00224-007-9017-6","article-title":"Coinduction for exact real number computation","volume":"43","author":"Berger","year":"2008","journal-title":"Theory of Computing Systems"},{"key":"2025090809272766600_ref3","article-title":"Extracting non-deterministic concurrent programs","volume-title":"25th EACSL Annual Conference on Computer Science Logic (CSL 2016)","author":"Berger","year":"2016"},{"key":"2025090809272766600_ref4","doi-asserted-by":"crossref","first-page":"102903","DOI":"10.1016\/j.apal.2020.102903","article-title":"Intuitionistic fixed point logic","volume":"172","author":"Berger","year":"2021","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025090809272766600_ref5","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/S1571-0661(05)80642-5","article-title":"Developing Theories of Types and Computability via Realizability","volume":"34","author":"Birkedal","year":"2020","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2025090809272766600_ref6","volume-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"2025090809272766600_ref7","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/978-3-642-02614-0_10","article-title":"Combining Coq and Gappa for certifying floating-point programs","volume-title":"Intelligent Computer Mathematics","author":"Boldo","year":"2009"},{"key":"2025090809272766600_ref8","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1109\/ARITH.2011.40","article-title":"Flocq: A unified library for proving floating-point algorithms in Coq","volume-title":"2011 IEEE 20th Symposium on Computer Arithmetic","author":"Boldo","year":"2011"},{"key":"2025090809272766600_ref9","doi-asserted-by":"crossref","first-page":"1196","DOI":"10.1017\/S0960129514000437","article-title":"Formalization of real analysis: a survey of proof assistants and libraries","volume":"26","author":"Boldo","year":"2016","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025090809272766600_ref10","volume-title":"Computer Arithmetic and Formal Proofs - Verifying Floating-Point Algorithms with the Coq System","author":"Boldo","year":"2017"},{"key":"2025090809272766600_ref11","doi-asserted-by":"crossref","first-page":"1745","DOI":"10.1109\/TC.2019.2917902","article-title":"Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods","volume":"69","author":"Boldo","year":"2019","journal-title":"IEEE Transactions on Computers"},{"key":"2025090809272766600_ref12","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1006\/jcom.1998.0488","article-title":"Feasible real random access machines","volume":"14","author":"Brattka","year":"1998","journal-title":"Journal of Complexity"},{"key":"2025090809272766600_ref13","doi-asserted-by":"crossref","DOI":"10.1142\/9789812704979_0005","article-title":"The emperor\u2019s new recursiveness: the epigraph of the exponential function in two models of computability","volume-title":"Words, Languages & Combinatorics III","author":"Brattka","year":"2003"},{"key":"2025090809272766600_ref14","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/978-3-031-14788-3_5","article-title":"Computer science for continuous data","volume-title":"Computer Algebra in Scientific Computing","author":"Brau\u00dfe","year":"2022"},{"key":"2025090809272766600_ref15","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/S0304-3975(98)00285-0","article-title":"Constructive mathematics: a foundation for computable analysis","volume":"219","author":"Bridges","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"2025090809272766600_ref16","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala","year":"2013"},{"key":"2025090809272766600_ref17","doi-asserted-by":"crossref","DOI":"10.1002\/9780470277980","volume-title":"Classical Algebra: Its Nature, Origins, and Uses","author":"Cooke","year":"2008"},{"key":"2025090809272766600_ref18","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","article-title":"C-CoRN, the constructive Coq repository at Nijmegen","volume-title":"International Conference on Mathematical Knowledge Management","author":"Cruz-Filipe","year":"2004"},{"key":"2025090809272766600_ref19","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1007\/s11075-019-00711-z","article-title":"Optimal inverse projection of floating-point addition","volume":"83","author":"Gallois-Wong","year":"2020","journal-title":"Numerical Algorithms"},{"key":"2025090809272766600_ref20","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1002\/malq.19990450202","article-title":"A real number structure that is effectively categorical","volume":"45","author":"Hertling","year":"1999","journal-title":"Mathematical Logic Quarterly"},{"key":"2025090809272766600_ref21","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/BFb0022273","article-title":"On the interpretation of type theory in locally cartesian closed categories","volume-title":"Computer Science Logic","author":"Hofmann","year":"1995"},{"key":"2025090809272766600_ref22","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"2025090809272766600_ref23","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-662-57669-4_13","article-title":"Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Kawamura","year":"2018"},{"key":"2025090809272766600_ref24","first-page":"9","article-title":"Verified exact real limit computation","volume-title":"Proceeding of the 15th International Conference on Computability and Complexity in Analysis (CCA)","author":"Kone\u010dn\u00fd","year":"2018"},{"key":"2025090809272766600_ref25","article-title":"Computable analysis for verified exact real computation","volume-title":"40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)","author":"Kone\u010dn\u00fd","year":"2020"},{"key":"2025090809272766600_ref26","article-title":"Aern2-real: A Haskell library for exact real number computation. Software available at","author":"Kone\u010dn\u00fd"},{"key":"2025090809272766600_ref27","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/978-3-030-88853-4_16","article-title":"Axiomatic reals and certified efficient exact real computation","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Kone\u010dn\u00fd","year":"2021"},{"key":"2025090809272766600_ref28","doi-asserted-by":"crossref","first-page":"771","DOI":"10.1007\/978-3-031-06773-0_41","article-title":"Certified computation of nondeterministic limits","volume-title":"NASA Formal Methods Symposium","author":"Kone\u010dn\u00fd","year":"2022"},{"key":"2025090809272766600_ref29","first-page":"215","article-title":"Computational complexity of real powering and improved solving linear differential equations","volume-title":"International Computer Science Symposium in Russia","author":"Koswara","year":"2019"},{"key":"2025090809272766600_ref30","first-page":"90","article-title":"Computer certified efficient exact reals in Coq","volume-title":"International Conference on Intelligent Computer Mathematics","author":"Krebbers","year":"2011"},{"key":"2025090809272766600_ref31","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(85)90208-7","article-title":"Theory of representations","volume":"38","author":"Kreitz","year":"1985","journal-title":"Theoretical Computer Science"},{"key":"2025090809272766600_ref32","volume-title":"Realizability Toposes and Language Semantics","author":"Longley","year":"1995"},{"key":"2025090809272766600_ref33","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(77)90048-2","article-title":"A fundamental effect in computations on real numbers","volume":"5","author":"Luckhardt","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"2025090809272766600_ref34","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-540-71070-7_2","article-title":"Proving bounds on real-valued functions with computations","volume-title":"International Joint Conference on Automated Reasoning","author":"Melquiond","year":"2008"},{"key":"2025090809272766600_ref35","doi-asserted-by":"crossref","first-page":"1692","DOI":"10.1017\/S0960129513000327","article-title":"Program extraction in exact real arithmetic","volume":"25","author":"Miyamoto","year":"2015","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025090809272766600_ref36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1353445.1353446","article-title":"The pitfalls of verifying floating-point computations","volume":"30","author":"Monniaux","year":"2008","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"2025090809272766600_ref37","article-title":"Implementing limits in an interactive RealRAM","volume-title":"3rd Conference on Real Numbers and Computers","author":"M\u00fcller"},{"key":"2025090809272766600_ref38","first-page":"222","article-title":"The iRRAM: exact arithmetic in C++","volume-title":"International Workshop on Computability and Complexity in Analysis","author":"M\u00fcller","year":"2000"},{"key":"2025090809272766600_ref39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jco.2017.08.003","article-title":"A topological view on algebraic computation models","volume":"44","author":"Neumann","year":"2018","journal-title":"Journal of Complexity"},{"key":"2025090809272766600_ref40","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1017\/S0960129506005871","article-title":"A monadic, functional implementation of real numbers","volume":"17","author":"O\u2019Connor","year":"2007","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025090809272766600_ref41","first-page":"246","article-title":"Certified exact transcendental real number computation in Coq","volume-title":"Theorem proving in higher order logics. Vol. 5170 of Lecture Notes in Computer Science","author":"O\u2019Connor","year":"2008"},{"key":"2025090809272766600_ref42","doi-asserted-by":"crossref","first-page":"3386","DOI":"10.1016\/j.tcs.2010.05.031","article-title":"A computer-verified monadic functional implementation of the integral","volume":"411","author":"O\u2019Connor","year":"2010","journal-title":"Theoretical Computer Science"},{"key":"2025090809272766600_ref43","doi-asserted-by":"crossref","DOI":"10.46298\/lmcs-20(2:17)2024","article-title":"Semantics, Specification Logic, and Hoare Logic of Exact Real Computation","volume-title":"Logical Methods in Computer Science","author":"Park"},{"key":"2025090809272766600_ref44","first-page":"11","article-title":"Intensionality and multi-valued limits","volume-title":"Proceeding of the 15th International Conference on Computability and Complexity in Analysis (CCA)","author":"Brau\u00dfe","year":"2018"},{"key":"2025090809272766600_ref45","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1016\/S1571-0661(04)00108-2","article-title":"Realizability models for type theories","volume":"23","author":"Reus","year":"1999","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2025090809272766600_ref46","doi-asserted-by":"crossref","article-title":"QED at large: A survey of engineering of formally verified software","author":"Ringer","DOI":"10.1561\/9781680835953"},{"key":"2025090809272766600_ref47","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1002\/1521-3870(200210)48:1+<78::AID-MALQ78>3.0.CO;2-K","article-title":"Effectivity in spaces with admissible multirepresentations","volume":"48","author":"Schr\u00f6der","year":"2002","journal-title":"Mathematical Logic Quarterly: Mathematical Logic Quarterly"},{"key":"2025090809272766600_ref48","first-page":"323","article-title":"Constructive analysis with witnesses","volume-title":"Proof Technology and Computation. Nato Science Series","author":"Schwichtenberg","year":"2006"},{"key":"2025090809272766600_ref50","doi-asserted-by":"crossref","first-page":"145","DOI":"10.2307\/2267043","article-title":"Nicht konstruktiv beweisbare S\u00e4tze der analysis","volume":"14","author":"Specker","year":"1949","journal-title":"The Journal of Symbolic Logic"},{"key":"2025090809272766600_ref51","article-title":"Computable analysis and notions of continuity in Coq","volume":"17","author":"Steinberg","year":"2021","journal-title":"Logical Methods in Computer Science"},{"key":"2025090809272766600_ref52","doi-asserted-by":"crossref","volume-title":"Semantics of Type Theory: Correctness, Completeness and Independence Results","author":"Streicher","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"2025090809272766600_ref53","volume-title":"Realizability: An Introduction to its Categorical Side","author":"Van Oosten","year":"2008"},{"key":"2025090809272766600_ref54","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-56999-9","volume-title":"Computable Analysis","author":"Weihrauch","year":"2000"},{"key":"2025090809272766600_ref55","volume-title":"A Continuous Computational Interpretation of Type Theories","author":"Xu","year":"2015"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/6\/exae066\/59836230\/exae066.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/6\/exae066\/59836230\/exae066.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T13:28:34Z","timestamp":1757338114000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/doi\/10.1093\/logcom\/exae066\/7824790"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,18]]},"references-count":54,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,7,29]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exae066","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2025,9]]},"published":{"date-parts":[[2024,10,18]]},"article-number":"exae066"}}