Hostname: page-component-8448b6f56d-wq2xx Total loading time: 0 Render date: 2024-04-24T09:21:06.471Z Has data issue: false hasContentIssue false
  • English
  • Français

Constructive analysis, types and exact real numbers

Published online by Cambridge University Press:  01 February 2007

HERMAN GEUVERS ,
MILAD NIQUI ,
BAS SPITTERS  and
FREEK WIEDIJK
HERMAN GEUVERS
Affiliation:
Radboud University Nijmegen, the Netherlands Email: spitters@cs.ru.nl
MILAD NIQUI
Affiliation:
Radboud University Nijmegen, the Netherlands Email: spitters@cs.ru.nl
BAS SPITTERS
Affiliation:
Radboud University Nijmegen, the Netherlands Email: spitters@cs.ru.nl
FREEK WIEDIJK
Affiliation:
Radboud University Nijmegen, the Netherlands Email: spitters@cs.ru.nl
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 17 , Issue 1 , February 2007 , pp. 3 - 36
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aberth, O. (1980) Computable Analysis, McGraw-Hill.Google Scholar
Abramsky, S. and Jung, A. (1994) Domain theory. In: Abramsky, S., Gabbay, D. M. and Maibaum, T. S. E. (eds.) Handbook of logic in computer science (vol. 3): semantic structures, Oxford University Press 1–168.Google Scholar
Barendregt, H. and Geuvers, H. (2001) Proof-assistants using dependent type systems. In: Handbook of automated reasoning, Elsevier Science Publishers 1149–1238.CrossRefGoogle Scholar
Barendregt, H. P. (1992) Lambda calculi with types. In: Handbook of logic in computer science (vol. 2): background, computational structures, Oxford University Press 117–309.Google Scholar
Barwise, J. and Moss, L. (1996) Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena, CSLI Publications, Stanford, California.Google Scholar
Bauer, A. (2000) The Realizability Approach to Computable Analysis and Topology, Ph.D. thesis, Carnegie Mellon University.Google Scholar
Bauer, A. (2005) Realizability as the connection between computable and constructive mathematics. (Available at http://math.andrej.com/category/papers/.)Google Scholar
Bauer, A., Escardó, M. and Simpson, A. (2002) Comparing functional paradigms for exact real-number computation. In: Automata, languages and programming. Springer-Verlag Lecture Notes in Computer Science 2380489–500.Google Scholar
Beeson, M. J. (1985) Foundations of constructive mathematics, Springer-Verlag.CrossRefGoogle Scholar
Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M. and Zuber, W. (1998) Proof theory at work: Program development in the Minlog system. In: Bibel, W. and Schmidt, P. H. (eds.) Automated Deduction: A Basis for Applications. Volume II, Systems and Implementation Techniques, Kluwer Academic Publishers.Google Scholar
Berger, U., Buchholz, W. and Schwichtenberg, H. (2002) Refined Program Extraction from Classical Proofs. Annals of Pure and Applied Logic 114 3–25.Google Scholar
Berghofer, S. (2003) Proofs, Programs and Executable Specifications in Higher Order Logic, Ph.D. thesis, Institut für Informatik, Technische Universität München.Google Scholar
Bertot, Y. (2005) Filters on coinductive streams, an application to eratosthenes' sieve. In: Urzyczyn, P. (ed.) Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005. Springer-Verlag Lecture Notes in Computer Science 3461 102–115.Google Scholar
Birkedal, L. (2000) Developing theories of types and computability via realizability. Electronic Notes in Theoretical Computer Science 34.Google Scholar
Bishop, E. (1967) Foundations of constructive analysis, McGraw-Hill.Google Scholar
Bishop, E. and Bridges, D. (1985) Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer-Verlag.CrossRefGoogle Scholar
Boehm, H.-J. (2005) Constructive Reals Calculator. (Available at http://www.hpl.hp.com/personal/Hans_Boehm/crcalc/.)Google Scholar
Boehm, H.-J., Cartwright, R., Riggle, M. and O'Donnell, M. J. (1986) Exact real arithmetic: A case study in higher order programming. In: Proceedings of the 1986 ACM conference on LISP and functional programming, ACM Press 162–173.Google Scholar
Bove, A. and Capretta, V. (2005) Modelling general recursion in type theory. Mathematical Structures in Computer Science 15 (4)671–708.CrossRefGoogle Scholar
Brezinski, C. (1991) History of Continued Fractions and Padé Approximants, Springer-Verlag Series in Computational Mathematics 12.CrossRefGoogle Scholar
Bridges, D. and Richman, F. (1987) Varieties in Constructive Mathematics, London Mathematical Society Lecture Notes Series 97, Cambridge University Press.CrossRefGoogle Scholar
Bridges, D. and Vita, L. (to appear). Techniques of Constructive Analysis, Springer-Verlag Universitext.Google Scholar
Brouwer, L. (1975) Collected Works, North-Holland.Google Scholar
Brouwer, L. E. J. (1921) Besitzt jede reelle Zahl eine Dezimalbruchentwicklung? Math. Ann. 83 (3–4)201–210.Google Scholar
Brouwer, L. E. J. (1927) Über Definitionsbereiche von Funktionen. Math. Ann. 97 (1)60–75.CrossRefGoogle Scholar
Ceitin, G. S. (1959) Algorithmic operators in constructive complete separable metric spaces. Dokl. Akad. Nauk SSSR 128 49–52.Google Scholar
Ceitin, G. S. (1962) Algorithmic operators in constructive metric spaces. Trudy Mat. Inst. Steklov. 67 295–361.Google Scholar
Constable, R. L., Allen, S. F., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D. J., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J. T. and Smith, S. F. (1986) Implementing Mathematics with the Nuprl Development System, Prentice-Hall.Google Scholar
Coq Development Team (2004) The Coq Proof Assistant Reference Manual. (Available at ftp://ftp.inria.fr/INRIA/coq/current/doc/Reference-Manual.ps.gz.)Google Scholar
Coquand, T. (1994) Infinite objects in type theory. In: Barendregt, H. and Nipkow, T. (eds.) Types for Proofs and Programs, International Workshop, TYPES'93. Springer-Verlag Lecture Notes in Computer Science 80662–78.CrossRefGoogle Scholar
Coquand, T. and Paulin, C. (1990) Inductively defined types. In: COLOG-88: Proceedings of the international conference on computer logic, Springer-Verlag 50–66.CrossRefGoogle Scholar
Crosilla, L. and Schuster, P. (2005) From Sets and Types to Topology and Analysis – Towards Practicable Foundations for Constructive Mathematics, Oxford Logic Guides 48, Oxford University Press.Google Scholar
Cruz-Filipe, L., Geuvers, H. and Wiedijk, F. (2004) C-CoRN: the Constructive Coq Repository at Nijmegen. In: Asperti, A., Bancerek, G. and Trybulec, A. (eds.) Mathematical Knowledge Management, Proceedings of MKM 2004. Springer-Verlag Lecture Notes in Computer Science 311988–103.Google Scholar
Cruz-Filipe, L. and Letouzey, P. (2005) A Large-Scale Experiment in Executing Extracted Programs. Electronic Notes in Theoretical Computer Science.Google Scholar
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–220.Google Scholar
De Bruijn, N. G. (1980) A survey of the project AUTOMATH. In: Hindley, J. R. and Seldin, J. P. (eds.) Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press 580–606.Google Scholar
Di Gianantonio, P. (1996) A golden ratio notation for the real numbers. Technical Report CS-R9602, Centrum voor Wiskunde en Informatica (CWI).Google Scholar
Di Gianantonio, P. and Miculan, M. (2003) A unifying approach to recursive and co-recursive definitions. In: Geuvers, H. and Wiedijk, F. (eds.) Types for Proofs and Programs: International Workshop, TYPES 2002. Springer-Verlag Lecture Notes in Computer Science 2646148–161.CrossRefGoogle Scholar
Dijkstra, E. W. (1980) On the productivity of recursive definitions. Personal note EWD 749.Google Scholar
Du, Z., Eleftheriou, M., Moreira, J. E. and Yap, C. (2002) Hypergeometric functions in exact geometric computation. In: Brattka, V., Schröder, M. and Weihrauch, K. (eds.) CCA 2002 Computability and Complexity in Analysis. Electronic Notes in Theoretical Computer Science 66. (Also: 5th International Workshop, CCA 2002, Málaga, Spain, July 12–13 2002.)Google Scholar
Dybjer, P. (1997) Representing inductively defined sets by wellorderings in Martin-Löf's type theory. Theoretical Computer Science 176 (1–2)329–335.Google Scholar
Edalat, A. (1997) Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic 3 (4)401–452.Google Scholar
Edalat, A. (2005) Exact Computation – Implementations. (Available at http://www.doc.ic.ac.uk/~ae/exact-computation/#bm:implementations.)Google Scholar
Edalat, A. and Escardó, M. (1996) Integration in Real PCF (extended abstract). In: Proceedings of the 11th Annual IEEE Symposium on Logic In Computer Science 382–393.CrossRefGoogle Scholar
Edalat, A. and Heckmann, R. (2002) Computing with real numbers: (i) LFT approach to real computation, (ii) Domain-theoretic model of computational geometry. In: Barthe, G., Dybjer, P., Pinto, L. and Saraiva, J. (eds.) Applied Semantics. Springer-Verlag Lecture Notes in Computer Science 2395193–267.Google Scholar
Edalat, A. and Lieutier, A. (2004) Domain theory and differential calculus (functions of one variable). Mathematical Structures in Computer Science 14 (6)771–802.CrossRefGoogle Scholar
Edalat, A. and Potts, P. J. (1997) A new representation for exact real numbers. In: Brookes, S. and Mislove, M. (eds.) Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference (MFPS XIII). Electronic Notes in Theoretical Computer Science 6.Google Scholar
Edalat, A., Potts, P. J. and Sünderhauf, P. (1999) Lazy computation with exact real numbers. In: Berman, M. and Berman, S. (eds.) Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP-98). ACM SIGPLAN Notices 34 (1) 185–194.Google Scholar
Escardó, M. (1996) PCF extended with real numbers. Theoretical Computer Science 162 (1)79–115.Google Scholar
Escardó, M., Hofmann, M. and Streicher, T. (2004) On the non-sequential nature of the interval-domain model of real-number computation. Mathematical Structures in Computer Science 14 (6)803–814.Google Scholar
Escardó, M. and Streicher, T. (1999) Induction and recursion on the partial real line with applications to Real PCF. Theoretical Computer Science 210 (1)121–157.CrossRefGoogle Scholar
Filliâtre, J.-C. (2005) Constructive reals OCaml library. (Available at http://www.lri.fr/~filliatr/creal.en.html.)Google Scholar
Fourman, M. P. and Grayson, R. J. (1982) Formal spaces. In: The L. E. J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics 110, North-Holland 107–122.Google Scholar
Geuvers, H. (1992) Inductive and coinductive types with iteration and recursion. In: Nordström, B., Pettersson, K. and Plotkin, G. (eds.) Informal Proc. of Workshop on Types for Proofs and Programs, Båstad, Sweden, 8–12 June 1992, Dept. of Computing Science, Chalmers Univ. of Technology and Göteborg Univ 193–217.Google Scholar
Geuvers, H. and Niqui, M. (2002) Constructive real numbers in Coq: Axioms and categoricity. In: Callaghan, P., Luo, Z., McKinna, J. and Pollack, R. (eds.) Types for Proofs and Programs: International Workshop, TYPES 2000. Springer-Verlag Lecture Notes in Computer Science 227779–95.Google Scholar
Giménez, 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élisme, Ecole Normale Supérieure de Lyon.Google Scholar
Gonthier, G. (2005) A computer-checked proof of the four colour theorem. Technical report, Microsoft Research Cambridge.Google Scholar
Gowland, P. and Lester, D. (2001) A survey of exact arithmetic implementations. In: Blanck, J., Brattka, V. and Hertling, P. (eds.) Computability and Complexity in Analysis: 4th International Workshop, CCA 2000. Springer-Verlag Lecture Notes in Computer Science 206430–47.CrossRefGoogle Scholar
Gunter, C. A. and Scott, D. S. (1990) Semantic domains. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), Elsevier 633–674.Google Scholar
Guy, M. (2005) bignum/BigFloat. (Available at http://medialab.freaknet.org/bignum/.)Google Scholar
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.Google Scholar
Hallnäs, L. (1990) On the syntax of infinite objects: an extension of Martin-Löf's theory of expressions. In: Martin-Löf, P. and Mints, G. (eds.) COLOG-88, International Conference on Computer Logic. Springer-Verlag Lecture Notes in Computer Science 41794–194.Google Scholar
Hanrot, G., Lefèvre, V., Pélissier, 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/.)Google Scholar
Harrison, J. (1994) Constructing the real numbers in HOL. Formal Methods in System Design 5 35–59.Google Scholar
Hayashi, S. and Nakano, H. (1987) PX, a Computational Logic. Technical report, Research Institute for Mathematical Sciences, Kyoto University.Google Scholar
Heyting, A. (1956) Intuitionism. An introduction, Studies in Logic and the Foundations of Mathematics, North-Holland.Google Scholar
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/.)Google Scholar
Howard, W. A. (1980) The formulae-as-types notion of construction. In: Hindley, J. R. and Seldin, J. P. (eds.) Essays on Combinatory Logic, Lambda Calculus and Formalism. Dedicated to Haskell B. Curry on the occasion of his 80th birthday, Academic Press 479–490.Google Scholar
Hughes, J. and Niqui, M. (2006) Admissible digit sets. Theoretical Computer Science 351 (1)61–73.Google Scholar
Hyland, J. (1982) The effective topos. In: Troelstra, A. and Dalen, D. V. (eds.) The L.E.J. Brouwer Centenary Symposium, North-Holland 165–216.Google Scholar
IEEE Task P754 (1985) IEEE standard for binary floating-point arithmetic. ACM SIGPLAN Notices 22 (2)9–25.Google Scholar
Jacobs, B. (1999) Categorical logic and type theory, Studies in Logic and the Foundations of Mathematics 141, North-Holland.Google Scholar
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.)Google Scholar
Jacobs, B. and Rutten, J. (1997) A tutorial on (co)algebras and (co)induction. Bulletin of the European Association for Theoretical Computer Science. EATCS 62 222–259.Google Scholar
Kearfott, B. R. (1996) Interval computations: Introduction, uses, and resources. Euromath Bulletin 2 (1)95–112.Google Scholar
Kleene, S. and Vesley, R. (1965) The foundations of intuitionistic mathematics, especially in relation to recursive functions, North-Holland.Google Scholar
Knuth, D. E. (1997) The Art of Computer Programming volume 2: Seminumerical Algorithms, 3rd edition, Addison-Wesley.Google Scholar
Konečný, M. (2000) Many-Valued Real Functions Computable by Finite Transducers using IFS-Representations, Ph.D. thesis, School of Computer Science, The University of Birmingham.Google Scholar
Kornerup, P. and Matula, D. (1988) An on-line arithmetic unit for bit-pipelined rational arithmetic. Journal of Parallel and Distributed Computing 5 310–330.Google Scholar
Krämer, W. (1997) A priori worst-case error bounds for floating-point computations. In: Lang, T., Muller, J.-M. and Takagi, N. (eds.) 13th IEEE Symposium on Computer Arithmetic. Symposium on Computer Arithmetic 1364–73.Google Scholar
Kreckel, R. (2005) CLN – Class Library for Numbers. (Available at http://www.ginac.de/CLN/.)Google Scholar
Kreisel, G., Lacombe, D. and Shoenfield, J. R. (1957a) Fonctionnelles récursivement définissables et fonctionnelles récursives. C. R. Acad. Sci. Paris 245 399–402.Google Scholar
Kreisel, G., Lacombe, D. and Shoenfield, J. R. (1957b) Partial recursive functionals and effective operations. In: Constructivity in mathematics: Proceedings of the colloquium held at Amsterdam 1957 (edited by A. Heyting), Studies in Logic and the Foundations of Mathematics, North-Holland 290–297.Google Scholar
Lambek, J. and Scott, P. J. (1988) Introduction to higher order categorical logic (reprint of the 1986 original), Cambridge Studies in Advanced Mathematics 7, Cambridge University Press.Google Scholar
Lambov, B. (2005) The RealLib Project. (Available at http://www.brics.dk/~barnie/RealLib/.)Google Scholar
Lester, D. (2001) Effective continued fractions. In: Burgess, N. and Ciminiera, L. (eds.) 15th IEEE Symposium on Computer Arithmetic, IEEE Computer Society Press 163–172.Google Scholar
Lester, D. (2005) Exact Arithmetic Implementations. (Available at http://www.cs.man.ac.uk/arch/dlester/exact.html.)Google Scholar
Letouzey, P. (2004) Programmation fonctionnelle certifiée – L'extraction de programmes dans l'assistant Coq, Ph.D. thesis, Université de Paris XI Orsay.Google Scholar
Lietz, P. (2004) From Constructive Mathematics to Computable Analysis via the Realizability Interpretation, Ph.D. thesis, Darmstadt University of Technology.Google Scholar
Lindström, I. (1989) A construction of non-well-founded sets within Martin-Löf's type theory. Journal of Symbolic Logic 54 (1)57–64.Google Scholar
Luo, Z. (1994) Computation and reasoning: a type theory for computer science, Oxford University Press.CrossRefGoogle Scholar
Martin-Löf, P. (1984) Intuitionistic type theory, Studies in Proof Theory 1, Bibliopolis.Google Scholar
Martin-Löf, P. (1990) Mathematics of infinity. In: Martin-Löf, P. and Mints, G. (eds.) COLOG-88, International Conference on Computer Logic Springer-Verlag Lecture Notes in Computer Science 417149–197.Google Scholar
Mencer, O. (2000) Rational Arithmetic Units in Computer Systems, Ph.D. thesis, Stanford University.Google Scholar
Mendler, N. P. (1991) Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic 51 159–172.Google Scholar
Mendler, N. P., Panangaden, P. and Constable, R. L. (1986) Infinite objects in type theory. In: Symposium on Logic in Computer Science (LICS '86), IEEE Computer Society Press 249–255.Google Scholar
Ménissier-Morain, V. (1994) Arithmétique exacte, conception, algorithmique et performances d'une implémentation informatique en précision arbitraire, Thèse, Université Paris 7.Google Scholar
Monagan, M., Geddes, K., Heal, K., Labahn, G. and Vorkoetter, S. (1997) Maple V Programming Guide for Release 5, Springer-Verlag.Google Scholar
Müller, N. (2005) iRRAM – Exact Arithmetic in C++. (Available at http://www.informatik.uni-trier.de/iRRAM/.)Google Scholar
Müller, N. T. (2001) The iRRAM: Exact arithmetic in C++. In: Blanck, J., Brattka, V. and Hertling, P. (eds.) Computability and Complexity in Analysis: 4th International Workshop, CCA 2000. Springer-Verlag Lecture Notes in Computer Science 2064222–252.Google Scholar
Nipkow, T., Paulson, L. and Wenzel, M. (2002) Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer-Verlag Lecture Notes in Computer Science 2283.Google Scholar
Niqui, M. (2004) Formalising Exact Arithmetic: Representations, Algorithms and Proofs, Ph.D. thesis, Radboud Universiteit Nijmegen.Google Scholar
Niqui, M. (2005) Formalising exact arithmetic in type theory. In: Cooper, S. B., Löwe, B. and Torenvliet, L. (eds.) New Computational Paradigms: First Conference on Computability in Europe, CiE 2005. Springer-Verlag Lecture Notes in Computer Science 3526368–377.Google Scholar
Nordström, B., Peterson, K. and Smith, J. M. (1990) Programming in Martin-Löf's Type Theory: an introduction, Oxford Science Publications.Google Scholar
O'Connor, R. (2005) Few Digits 0.4.0. (Available at http://r6.ca/FewDigits/.)Google Scholar
Pattinson, D. (2003) Computable functions on final coalgebras. In: Proc. of 6th Workshop on Coalgebraic Methods in Computer Science, CMCS'03. Electronic Notes in Theoretical Computer Science 82 (1).Google Scholar
Paulin-Mohring, C. (1993) Inductive definitions in the system Coq – rules and properties. In: Bezem, M. and Groote, J. F. (eds.) Proceedings of the 1st TLCA conference. Springer-Verlag Lecture Notes in Computer Science 664328–345.Google Scholar
Pfenning, F. (2001) Logical frameworks. In: Handbook of Automated Reasoning, Elsevier Science Publishers 1063–1147.CrossRefGoogle Scholar
Pierce, B. C. (2002) Types and Programming Languages, MIT Press.Google Scholar
Plotkin, G. D. (1977) LCF considered as a programming language. Theoretical Computer Science 5 (3)225–255.CrossRefGoogle Scholar
Potts, P. J. (1998) Exact Real Arithmetic using Möbius Transformations, Ph.D. thesis, University of London, Imperial College.Google Scholar
Potts, P. J. and Edalat, A. (1997) Exact real computer arithmetic. Technical Report DOC 97/9, Department of Computing, Imperial College.Google Scholar
Rutten, J. J. M. M. (2000) Universal coalgebra: a theory of systems. Theoretical Computer Science 249 (1)3–80.Google Scholar
Sambin, G. (1987) Intuitionistic formal spaces – a first communication. In: Skordev, D. (ed.) Mathematical logic and its Applications, Plenum 187–204.Google Scholar
Sambin, G. (2000) Formal topology and domains. In: Remagen-Rolandseck, 1998. Electronic notes in theoretical computer science 35.Google Scholar
Sambin, G., Valentini, S. and Virgili, P. (1996) Constructive domain theory as a branch of intuitionistic pointfree topology. Theoretical Computer Science 159 (2)319–341.Google Scholar
Schwarz, J. (1989) Implementing Infinite Precision Arithmetic. In: Proc. 9th IEEE Symposium on Computer Arithmetic 10–17.Google Scholar
Scott, D. (1970) Constructive validity. In: Lacombe, D. and Laudelt, M. (eds.) Symposium on Automatic Demonstration. Springer-Verlag Lecture Notes in Mathematics 237–275.Google Scholar
Scott, D. (1972) Lattice theory, data types, and semantics. In: Rustin, R. (ed.) Formal Semantics of Programming Languages, Courant Computer Science Symposia 2, Prentice-Hall 65–106.Google Scholar
Scott, D. (1976) Data types as lattices. SIAM J. Comput. 5 (3)522–587.Google Scholar
Sijtsma, B. A. (1989) On the productivity of recursive list definitions. ACM Trans. Program. Lang. Syst. (TOPLAS) 11 (4)633–649.Google Scholar
Simpson, A. K. (1998) Lazy functional algorithms for exact real functionals. In: Brim, L., Gruska, J. and Zlatuska, J. (eds.) Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS'98. Springer-Verlag Lecture Notes in Computer Science 1450456–464.Google Scholar
Telford, A. and Turner, D. (2000) Ensuring Termination in ESFP. Journal of Universal Computer Science 6 (4)474–488.Google Scholar
Troelstra, A. and van Dalen, D. (1988a) Constructivism in mathematics. An introduction, Studies in Logic and the Foundations of Mathematics 123, North-Holland.Google Scholar
Troelstra, A. S. (1977) Choice sequences: A chapter of intuitionistic mathematics, Oxford Logic Guides, Clarendon Press.Google Scholar
Troelstra, A. S. (1992) Comparing the theory of representations and constructive mathematics. In: Computer science logic (Berne 1991). Springer-Verlag Lecture Notes in Computer Science 626 382–395.Google Scholar
Troelstra, A. S. (1998) Realizability. In: Handbook of proof theory, Studies in Logic and the Foundations of Mathematics 137, North-Holland 407–473.Google Scholar
Troelstra, A. S. and van Dalen, D. (1988b) Constructivism in Mathematics: An Introduction, vol I, Studies in Logic and the Foundations of Mathematics 121, North-Holland.Google Scholar
van Oosten, J. (2002) Realizability: a historical essay. Realizability (Trento 1999). Mathematical Structures in Computer Science 12 (3)239–263.Google Scholar
Vuillemin, J. E. (1990) Exact real computer arithmetic with continued fractions. IEEE Transactions on Computers 39 (8)1087–1105.Google Scholar
Weihrauch, K. (1997) A foundation for computable analysis. In: Plášil, F. and Jeffery, K. G. (eds.) Theory and Practice of Informatics, 24th Seminar on Current Trends in Theory and Practice of Informatics. Springer-Verlag Lecture Notes in Computer Science 1338104–121.Google Scholar
Weihrauch, K. (2000) Computable Analysis: An introduction, Springer-Verlag.CrossRefGoogle Scholar
Weihrauch, K. and Kreitz, C. (1987) Representations of the real numbers and of the open subsets of the set of real numbers. Annals of Pure and Applied Logic 35 247–260.Google Scholar
Wolfram, S. (1996) The Mathematica book, Cambridge University Press.Google Scholar
Yap, C. and Dubé, T. (1995) The exact computation paradigm. In: Du, D.-Z. and Hwang, F. (eds.) Computing in Euclidean Geometry, 2nd edition, World Scientific Press.Google Scholar