{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,23]],"date-time":"2024-07-23T20:28:04Z","timestamp":1721766484976},"reference-count":135,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,2]]},"abstract":"<jats:p>In this paper we will discuss various aspects of computable\/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real arithmetic varying from concrete implementations, representation and algorithms to various models for real computation. We then put these models in a uniform framework using realisability, which opens the door to the use of type theoretic and coalgebraic constructions both in computing and reasoning about these computations. We will indicate that it is often natural to use constructive logic to reason about these computations.<\/jats:p>","DOI":"10.1017\/s0960129506005834","type":"journal-article","created":{"date-parts":[[2007,3,7]],"date-time":"2007-03-07T10:59:58Z","timestamp":1173265198000},"page":"3-36","source":"Crossref","is-referenced-by-count":19,"title":["Constructive analysis, types and exact real numbers"],"prefix":"10.1017","volume":"17","author":[{"given":"HERMAN","family":"GEUVERS","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MILAD","family":"NIQUI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"BAS","family":"SPITTERS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"FREEK","family":"WIEDIJK","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2007,2,1]]},"reference":[{"key":"S0960129506005834_rf135","volume-title":"Computing in Euclidean Geometry","author":"Yap","year":"1995"},{"key":"S0960129506005834_rf134","volume-title":"The Mathematica book","author":"Wolfram","year":"1996"},{"key":"S0960129506005834_rf133","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(87)90065-0"},{"key":"S0960129506005834_rf132","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-56999-9"},{"key":"S0960129506005834_rf131","first-page":"104","volume-title":"Theory and Practice of Informatics, 24th Seminar on Current Trends in Theory and Practice of Informatics","author":"Weihrauch","year":"1997"},{"key":"S0960129506005834_rf130","doi-asserted-by":"publisher","DOI":"10.1109\/12.57047"},{"key":"S0960129506005834_rf129","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003626"},{"key":"S0960129506005834_rf126","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023783"},{"key":"S0960129506005834_rf125","volume-title":"Choice sequences: A chapter of intuitionistic mathematics","author":"Troelstra","year":"1977"},{"key":"S0960129506005834_rf121","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69563"},{"key":"S0960129506005834_rf119","first-page":"65","volume-title":"Formal Semantics of Programming Languages","author":"Scott","year":"1972"},{"key":"S0960129506005834_rf118","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060636"},{"key":"S0960129506005834_rf116","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00169-7"},{"key":"S0960129506005834_rf115","volume-title":"Formal topology and domains","author":"Sambin","year":"2000"},{"key":"S0960129506005834_rf114","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0897-3_12"},{"key":"S0960129506005834_rf113","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129506005834_rf112","unstructured":"Potts P. J. and Edalat A. (1997) Exact real computer arithmetic. Technical Report DOC 97\/9, Department of Computing, Imperial College."},{"key":"S0960129506005834_rf111","unstructured":"Potts P. J. (1998) Exact Real Arithmetic using M\u00f6bius Transformations, Ph.D. thesis, University of London, Imperial College."},{"key":"S0960129506005834_rf110","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129506005834_rf128","volume-title":"Constructivism in Mathematics: An Introduction, vol I","author":"Troelstra","year":"1988"},{"key":"S0960129506005834_rf109","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0960129506005834_rf107","first-page":"328","volume-title":"Proceedings of the 1st TLCA conference","author":"Paulin-Mohring","year":"1993"},{"key":"S0960129506005834_rf106","volume-title":"Proc. of 6th Workshop on Coalgebraic Methods in Computer Science, CMCS'03","author":"Pattinson","year":"2003"},{"key":"S0960129506005834_rf103","doi-asserted-by":"publisher","DOI":"10.1007\/11494645_46"},{"key":"S0960129506005834_rf28","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"Constable","year":"1986"},{"key":"S0960129506005834_rf96","first-page":"249","volume-title":"Symposium on Logic in Computer Science (LICS '86)","author":"Mendler","year":"1986"},{"key":"S0960129506005834_rf63","unstructured":"Hanrot G. , Lef\u00e8vre V. , P\u00e9lissier P. , Zimmermann P. , Boldo S. , Daney D. , Dutour M. , Jeandel E. , Fousse L. , Rouillier F. and Ryde K. (2005) The MPFR Library. (Available at http:\/\/www.mpfr.org\/.)"},{"key":"S0960129506005834_rf124","volume-title":"Constructivism in mathematics. An introduction","author":"Troelstra","year":"1988"},{"key":"S0960129506005834_rf91","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and reasoning: a type theory for computer science","author":"Luo","year":"1994"},{"key":"S0960129506005834_rf12","unstructured":"Berghofer S. (2003) Proofs, Programs and Executable Specifications in Higher Order Logic, Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen."},{"key":"S0960129506005834_rf122","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055795"},{"key":"S0960129506005834_rf82","first-page":"399","article-title":"Fonctionnelles r\u00e9cursivement d\u00e9finissables et fonctionnelles r\u00e9cursives","volume":"245","author":"Kreisel","year":"1957","journal-title":"C. R. Acad. Sci. Paris"},{"key":"S0960129506005834_rf11","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00073-2"},{"key":"S0960129506005834_rf68","first-page":"479","volume-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism. Dedicated to Haskell B. Curry on the occasion of his 80th birthday","author":"Howard","year":"1980"},{"key":"S0960129506005834_rf61","unstructured":"Hagino T. (1987) A Categorical Programming Language. Ph.D. thesis CST-47-87, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh."},{"key":"S0960129506005834_rf14","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80642-5"},{"key":"S0960129506005834_rf36","first-page":"580","volume-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"De Bruijn","year":"1980"},{"key":"S0960129506005834_rf102","doi-asserted-by":"crossref","unstructured":"Niqui M. (2004) Formalising Exact Arithmetic: Representations, Algorithms and Proofs, Ph.D. thesis, Radboud Universiteit Nijmegen.","DOI":"10.1007\/11494645_46"},{"key":"S0960129506005834_rf74","first-page":"222","article-title":"A tutorial on (co)algebras and (co)induction","volume":"62","author":"Jacobs","year":"1997","journal-title":"Bulletin of the European Association for Theoretical Computer Science. EATCS"},{"key":"S0960129506005834_rf58","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45335-0_3"},{"key":"S0960129506005834_rf95","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"S0960129506005834_rf127","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80021-9"},{"key":"S0960129506005834_rf70","first-page":"165","volume-title":"The L.E.J. Brouwer","author":"Hyland","year":"1982"},{"key":"S0960129506005834_rf97","unstructured":"M\u00e9nissier-Morain V. (1994) Arithm\u00e9tique exacte, conception, algorithmique et performances d'une impl\u00e9mentation informatique en pr\u00e9cision arbitraire, Th\u00e8se, Universit\u00e9 Paris 7."},{"key":"S0960129506005834_rf25","doi-asserted-by":"publisher","DOI":"10.1007\/BF01447860"},{"key":"S0960129506005834_rf27","first-page":"295","article-title":"Algorithmic operators in constructive metric spaces","volume":"67","author":"Ceitin","year":"1962","journal-title":"Trudy Mat. Inst. Steklov."},{"key":"S0960129506005834_rf85","unstructured":"Lambov B. (2005) The RealLib Project. (Available at http:\/\/www.brics.dk\/~barnie\/RealLib\/.)"},{"key":"S0960129506005834_rf90","doi-asserted-by":"publisher","DOI":"10.2307\/2275015"},{"key":"S0960129506005834_rf101","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"S0960129506005834_rf47","volume-title":"Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference (MFPS XIII)","author":"Edalat","year":"1997"},{"key":"S0960129506005834_rf1","volume-title":"Computable Analysis","author":"Aberth","year":"1980"},{"key":"S0960129506005834_rf93","first-page":"149","volume-title":"COLOG-88, International Conference on Computer Logic","author":"Martin-L\u00f6f","year":"1990"},{"key":"S0960129506005834_rf22","volume-title":"Techniques of Constructive Analysis","author":"Bridges"},{"key":"S0960129506005834_rf3","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50020-5"},{"key":"S0960129506005834_rf73","unstructured":"Jacobs B. (2005) Introduction to Coalgebra. Towards Mathematics of States and Observations. (Draft available at http:\/\/www.cs.ru.nl\/B.Jacobs\/CLG\/JacobsCoalgebraIntro.pdf.)"},{"key":"S0960129506005834_rf40","volume-title":"CCA 2002 Computability and Complexity in Analysis","author":"Du","year":"2002"},{"key":"S0960129506005834_rf60","unstructured":"Guy M. (2005) bignum\/BigFloat. (Available at http:\/\/medialab.freaknet.org\/bignum\/.)"},{"key":"S0960129506005834_rf105","unstructured":"O'Connor R. (2005) Few Digits 0.4.0. (Available at http:\/\/r6.ca\/FewDigits\/.)"},{"key":"S0960129506005834_rf41","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00145-4"},{"key":"S0960129506005834_rf94","unstructured":"Mencer O. (2000) Rational Arithmetic Units in Computer Systems, Ph.D. thesis, Stanford University."},{"key":"S0960129506005834_rf54","unstructured":"Geuvers H. (1992) Inductive and coinductive types with iteration and recursion. In: Nordstr\u00f6m B. , Pettersson K. and Plotkin G. (eds.) Informal Proc. of Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, 8\u201312 June 1992, Dept. of Computing Science, Chalmers Univ. of Technology and G\u00f6teborg Univ 193\u2013217."},{"key":"S0960129506005834_rf33","first-page":"88","volume-title":"Mathematical Knowledge Management, Proceedings of MKM 2004","author":"Cruz-Filipe","year":"2004"},{"key":"S0960129506005834_rf108","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"S0960129506005834_rf62","first-page":"94","volume-title":"COLOG-88, International Conference on Computer Logic","author":"Halln\u00e4s","year":"1990"},{"key":"S0960129506005834_rf39","unstructured":"Dijkstra E. W. (1980) On the productivity of recursive definitions. Personal note EWD 749."},{"key":"S0960129506005834_rf56","unstructured":"Gim\u00e9nez E. (1996) Un Calcul de Constructions Infinies et son Application a la Verification des Systemes Communicants, Ph.D. thesis, PhD 96-11, Laboratoire de l'Informatique du Parall\u00e9lisme, Ecole Normale Sup\u00e9rieure de Lyon."},{"key":"S0960129506005834_rf98","volume-title":"Maple V Programming Guide for Release 5","author":"Monagan","year":"1997"},{"key":"S0960129506005834_rf4","first-page":"117","volume-title":"Handbook of logic in computer science (vol. 2): background, computational structures","author":"Barendregt","year":"1992"},{"key":"S0960129506005834_rf5","volume-title":"Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena","author":"Barwise","year":"1996"},{"key":"S0960129506005834_rf66","volume-title":"Intuitionism. An introduction","author":"Heyting","year":"1956"},{"key":"S0960129506005834_rf8","first-page":"489","volume-title":"Automata, languages and programming","author":"Bauer","year":"2002"},{"key":"S0960129506005834_rf84","volume-title":"Introduction to higher order categorical logic","author":"Lambek","year":"1988"},{"key":"S0960129506005834_rf6","unstructured":"Bauer A. (2000) The Realizability Approach to Computable Analysis and Topology, Ph.D. thesis, Carnegie Mellon University."},{"key":"S0960129506005834_rf7","unstructured":"Bauer A. (2005) Realizability as the connection between computable and constructive mathematics. (Available at http:\/\/math.andrej.com\/category\/papers\/.)"},{"key":"S0960129506005834_rf9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"S0960129506005834_rf13","first-page":"102","volume-title":"Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005","author":"Bertot","year":"2005"},{"key":"S0960129506005834_rf55","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_6"},{"key":"S0960129506005834_rf99","unstructured":"M\u00fcller N. (2005) iRRAM \u2013 Exact Arithmetic in C++. (Available at http:\/\/www.informatik.uni-trier.de\/iRRAM\/.)"},{"key":"S0960129506005834_rf15","volume-title":"Foundations of constructive analysis","author":"Bishop","year":"1967"},{"key":"S0960129506005834_rf16","doi-asserted-by":"crossref","unstructured":"Bishop E. and Bridges D. (1985) Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer-Verlag.","DOI":"10.1007\/978-3-642-61667-9"},{"key":"S0960129506005834_rf17","unstructured":"Boehm H.-J. (2005) Constructive Reals Calculator. (Available at http:\/\/www.hpl.hp.com\/personal\/Hans_Boehm\/crcalc\/.)"},{"key":"S0960129506005834_rf18","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319860"},{"key":"S0960129506005834_rf19","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"S0960129506005834_rf20","doi-asserted-by":"crossref","unstructured":"Brezinski C. (1991) History of Continued Fractions and Pad\u00e9 Approximants, Springer-Verlag Series in Computational Mathematics 12.","DOI":"10.1007\/978-3-642-58169-4"},{"key":"S0960129506005834_rf77","volume-title":"The Art of Computer Programming volume 2: Seminumerical Algorithms","author":"Knuth","year":"1997"},{"key":"S0960129506005834_rf21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565663"},{"key":"S0960129506005834_rf23","volume-title":"Collected Works","author":"Brouwer","year":"1975"},{"key":"S0960129506005834_rf24","doi-asserted-by":"publisher","DOI":"10.1007\/BF01458382"},{"key":"S0960129506005834_rf26","first-page":"49","article-title":"Algorithmic operators in constructive complete separable metric spaces","volume":"128","author":"Ceitin","year":"1959","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"S0960129506005834_rf117","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.1989.72804"},{"key":"S0960129506005834_rf29","unstructured":"Coq Development Team (2004) The Coq Proof Assistant Reference Manual. (Available at ftp:\/\/ftp.inria.fr\/INRIA\/coq\/current\/doc\/Reference-Manual.ps.gz.)"},{"key":"S0960129506005834_rf30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_72"},{"key":"S0960129506005834_rf31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"S0960129506005834_rf34","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe L. and Letouzey P. (2005) A Large-Scale Experiment in Executing Extracted Programs. Electronic Notes in Theoretical Computer Science.","DOI":"10.1016\/j.entcs.2005.11.024"},{"key":"S0960129506005834_rf35","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe L. and Spitters B. (2003) Program extraction from large proof developments. In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2000. Springer-Verlag Lecture Notes in Computer Science 205\u2013220.","DOI":"10.1007\/10930755_14"},{"key":"S0960129506005834_rf37","unstructured":"Di Gianantonio P. (1996) A golden ratio notation for the real numbers. Technical Report CS-R9602, Centrum voor Wiskunde en Informatica (CWI)."},{"key":"S0960129506005834_rf43","unstructured":"Edalat A. (2005) Exact Computation \u2013 Implementations. (Available at http:\/\/www.doc.ic.ac.uk\/~ae\/exact-computation\/#bm:implementations.)"},{"key":"S0960129506005834_rf38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"S0960129506005834_rf32","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566519.001.0001"},{"key":"S0960129506005834_rf42","doi-asserted-by":"publisher","DOI":"10.2307\/421098"},{"key":"S0960129506005834_rf44","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561453"},{"key":"S0960129506005834_rf123","first-page":"474","article-title":"Ensuring Termination in ESFP","volume":"6","author":"Telford","year":"2000","journal-title":"Journal of Universal Computer Science"},{"key":"S0960129506005834_rf45","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45699-6_5"},{"key":"S0960129506005834_rf48","first-page":"185","volume-title":"Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP-98)","author":"Edalat","year":"1999"},{"key":"S0960129506005834_rf49","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00250-2"},{"key":"S0960129506005834_rf2","first-page":"1","volume-title":"Handbook of logic in computer science (vol. 3): semantic structures","author":"Abramsky","year":"1994"},{"key":"S0960129506005834_rf50","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004360"},{"key":"S0960129506005834_rf46","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004359"},{"key":"S0960129506005834_rf51","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00099-1"},{"key":"S0960129506005834_rf78","unstructured":"Kone\u010dn\u00fd M. (2000) Many-Valued Real Functions Computable by Finite Transducers using IFS-Representations, Ph.D. thesis, School of Computer Science, The University of Birmingham."},{"key":"S0960129506005834_rf52","unstructured":"Filli\u00e2tre J.-C. (2005) Constructive reals OCaml library. (Available at http:\/\/www.lri.fr\/~filliatr\/creal.en.html.)"},{"key":"S0960129506005834_rf104","volume-title":"Programming in Martin-L\u00f6f's Type Theory: an introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0960129506005834_rf53","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70126-0"},{"key":"S0960129506005834_rf57","unstructured":"Gonthier G. (2005) A computer-checked proof of the four colour theorem. Technical report, Microsoft Research Cambridge."},{"key":"S0960129506005834_rf64","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384233"},{"key":"S0960129506005834_rf65","unstructured":"Hayashi S. and Nakano H. (1987) PX, a Computational Logic. Technical report, Research Institute for Mathematical Sciences, Kyoto University."},{"key":"S0960129506005834_rf67","unstructured":"Hofmann M. (1995) Extensional concepts in intensional type theory, Ph.D. thesis, Laboratory for Foundations of Computer Science, University of Edinburgh. (Available at http:\/\/www.lfcs.informatics.ed.ac.uk\/reports\/95\/ECS-LFCS-95-327\/.)"},{"key":"S0960129506005834_rf79","doi-asserted-by":"publisher","DOI":"10.1016\/0743-7315(88)90023-8"},{"key":"S0960129506005834_rf69","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.059"},{"key":"S0960129506005834_rf120","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"S0960129506005834_rf10","volume-title":"Automated Deduction: A Basis for Applications. Volume II, Systems and Implementation Techniques","author":"Benl","year":"1998"},{"key":"S0960129506005834_rf71","first-page":"9","article-title":"IEEE standard for binary floating-point arithmetic","volume":"22","year":"1985","journal-title":"ACM SIGPLAN Notices"},{"key":"S0960129506005834_rf72","volume-title":"Categorical logic and type theory","author":"Jacobs","year":"1999"},{"key":"S0960129506005834_rf59","first-page":"633","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)","author":"Gunter","year":"1990"},{"key":"S0960129506005834_rf75","first-page":"95","article-title":"Interval computations: Introduction, uses, and resources","volume":"2","author":"Kearfott","year":"1996","journal-title":"Euromath Bulletin"},{"key":"S0960129506005834_rf76","volume-title":"The foundations of intuitionistic mathematics, especially in relation to recursive functions","author":"Kleene","year":"1965"},{"key":"S0960129506005834_rf80","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.1997.614880"},{"key":"S0960129506005834_rf81","unstructured":"Kreckel R. (2005) CLN \u2013 Class Library for Numbers. (Available at http:\/\/www.ginac.de\/CLN\/.)"},{"key":"S0960129506005834_rf83","first-page":"290","volume-title":"Constructivity in mathematics: Proceedings of the colloquium held at Amsterdam 1957 (edited by A. Heyting)","author":"Kreisel","year":"1957"},{"key":"S0960129506005834_rf86","first-page":"163","volume-title":"15th IEEE Symposium on Computer Arithmetic","author":"Lester","year":"2001"},{"key":"S0960129506005834_rf87","unstructured":"Lester D. (2005) Exact Arithmetic Implementations. (Available at http:\/\/www.cs.man.ac.uk\/arch\/dlester\/exact.html.)"},{"key":"S0960129506005834_rf88","unstructured":"Letouzey P. (2004) Programmation fonctionnelle certifi\u00e9e \u2013 L'extraction de programmes dans l'assistant Coq, Ph.D. thesis, Universit\u00e9 de Paris XI Orsay."},{"key":"S0960129506005834_rf89","unstructured":"Lietz P. (2004) From Constructive Mathematics to Computable Analysis via the Realizability Interpretation, Ph.D. thesis, Darmstadt University of Technology."},{"key":"S0960129506005834_rf92","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0960129506005834_rf100","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45335-0_14"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129506005834","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,11]],"date-time":"2024-02-11T14:07:11Z","timestamp":1707660431000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129506005834\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":135,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2]]}},"alternative-id":["S0960129506005834"],"URL":"https:\/\/doi.org\/10.1017\/s0960129506005834","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}