References

[Bau00]

Andrej Bauer. The Realizability Approach to Computable Analysis and Topology. PhD thesis, Carnegie Mellon University, 2000. Available as CMU technical report CMU-CS-00-164.

[Bau08]

Andrej Bauer. Efficient computation with Dedekind reals. In Vasco Brattka, Ruth Dillhage, Tanja Grubba, and Angela Klutch, editors, Fifth International Conference on Computability and Complexity in Analysis, pages i–vi, Hagen, Germany, August 2008.

[BB08a]

Josef Berger and Douglas Bridges. The fan theorem and positive-valued uniformly continuous functions on compact intervals. New Zealand Journal of Mathematics, 38:129–135, 2008.

[BB08b]

Josef Berger and Douglas S. Bridges. The anti-Specker property, a Heine–Borel property, and uniform continuity. Archive for Mathematical Logic, 46:583–592, 2008.

[Bis67]

Errett A. Bishop. Foundations of Constructive Analysis. Higher Mathematics. McGraw–Hill, 1967.

[Bou66]

Nicolas Bourbaki. Topologie Générale. Hermann, 1966. English translation, “General Topology”, distrubuted by Springer-Verlag (1989).

[BR87]

Douglas S. Bridges and Fred Richman. Varieties of Constructive Mathematics. Number 97 in London Mathematical Society Lecture Notes. Cambridge University Press, 1987.

[Bri99]

Douglas S. Bridges. Constructive mathematics: a foundation for computable analysis. Theoretical Computer Science, 219:95–109, 1999.

[Cle87]

John C. Cleary. Logical arithmetic. Future Computing Systems, 2:125–149, 1987.

[CN96]

Jan Cederquist and Sara Negri. A constructive proof of the Heine–Borel covering theorem for formal reals. In Stefano Beradi and Mario Coppo, editors, Types for Proofs and Programs, number 1158 in Lecture Notes in Computer Science. Springer-Verlag, 1996.

[Con76]

John Horton Conway. On Numbers and Games. Number 6 in London Mathematical Society Monographs. Academic Press, 1976. Revised edition, 2001, published by A K Peters, Ltd.

[Ded72]

Richard Dedekind. Stetigkeit und irrationale Zahlen. Braunschweig, 1872. Reprinted in [Ded32], pages 315–334; English translation, Continuity and Irrational Numbers, in [Ded01].

[Ded01]

Richard Dedekind. Essays on the theory of numbers. Open Court, 1901. English translations by Wooster Woodruff Beman; republished by Dover, 1963.

[Ded32]

Richard Dedekind. Gesammelte mathematische Werke, volume 3. Vieweg, Braunschweig, 1932. Edited by Robert Fricke, Emmy Noether and �D8;ystein Ore; republished by Chelsea, New York, 1969.

[ES98]

Abbas Edalat and Philipp Sünderhauf. A domain-theoretic approach to real number computation. Theoretical Computer Science, 210:73–98, 1998.

[Esc04]

Martín Escardó. Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21–156, 2004.

[FH79]

Michael Fourman and J. Martin E. Hyland. Sheaf models for analysis. In Michael Fourman, Chris Mulvey, and Dana Scott, editors, Applications of Sheaves, number 753 in Lecture Notes in Mathematics, pages 280–301. Springer-Verlag, 1979.

[Fri58]

Richard Friedberg. Un contre-example relatif aux fonctionnelles récursives. Comptes rendus hebdomadaires des scéances de l’Académie des Sciences (Paris), 247:852–854, 1958.

[Gen35]

Gerhard Gentzen. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift, 39:176–210 and 405–431, 1935. English translation in [Gen69], pages 68–131.

[Gen69]

Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland, 1969. Edited by Manfred E. Szabo.

[GHK++80]

Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael Mislove, and Dana S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980. Second edition, Continuous Lattices and Domains, published by Cambridge University Press, 2003.

[Hey56]

Arend Heyting. Intuitionism, an Introduction. Studies in Logic and the Foundations of Mathematics. North-Holland, 1956. Third edition, 1971.

[HR90]

Martin Hyland and Giuseppe Rosolini. The discrete objects in the effective topos. Proceedings of the London Mathematical Society, 60:1–36, 1990.

[Hyl82]

J. Martin E. Hyland. The effective topos. In A. S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165–216. North Holland Publishing Company, 1982.

[Joh77]

Peter T. Johnstone. Topos Theory. Number 10 in London Mathematical Society Monographs. Academic Press, 1977.

[Joh82]

Peter T. Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Joh84]

Peter T. Johnstone. Open locales and exponentiation. Contemporary Mathematics, 30:84–116, 1984.

[JR84]

William Julian and Fred Richman. A uniformly continuous function on [0,1] that is everywhere different from its infimum. Pacific Journal of Mathematics, 111:333–340, 1984.

[JT84]

André Joyal and Myles Tierney. An extension of the Galois theory of Grothendieck. Memoirs of the American Mathematical Society, 51(309), 1984.

[Kau80]

Edgar Kaucher. Interval analysis in the extended interval space IR. In Götz Alefeld and Rolf Grigorieff, editors, Fundamentals of Numerical Computation, volume 2 of Computing. Supplementum. Springer-Verlag, 1980.

[Kea96]

Baker Kearfott. Interval computations: Introduction, uses and resources. Euromath Bulletin, 2(1):95–112, 1996.

[Kel86]

Max Kelly. A survey of totality in ordinary and enriched categories. Cahiers de Géometrie et Topologie Differentielle, 27:109–132, 1986.

[Kle45]

Stephen Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10:109–124, 1945.

[KNZ96]

Vladik Kreinovich, Vyacheslav Nesterov, and Nina Zheludeva. Interval methods that are guaranteed to underestimate (and the resulting new justification of Kaucher arithmetic). Reliable Computing, 2(2):119–124, 1996.

[Koc81]

Anders Kock. Synthetic Differential Geometry. Number 51 in London Mathematical Society Lecture Notes. Cambridge University Press, 1981. Second edition, number 333, 2006.

[Lak95]

Anatoly Lakeyev. Linear algebraic equations in Kaucher arithmetic. In Vladik Kreinovich, editor, Applications of Interval Computations (APIC’95), 1995. supplement to Reliable Computing.

[Moo66]

Ramon E. Moore. Interval Analysis. Automatic Computation. Prentice Hall, 1966. Second edition, Ramon Edgar Moore, Baker R Kearfott and Michael J Cloud, "Introduction to Interval Analysis", Society for Industrial and Applied Mathematics, Philadephia, 2009, ISBN 0989716691.

[Pal05]

Eric Palmgren. Continuity on the real line and in formal spaces. In Laura Crosilla and Peter Schuster, editors, From Sets and Types to Topology and Analysis: Towards Practicable Foundations of Constructive Mathematics, Oxford Logic Guides. Oxford University Press, 2005.

[Pea97]

Giuseppe Peano. Studii di logica matematica. Atti della Reale Accademia di Torino, 32:565–583, 1897. Reprinted in Peano, Opere Scelte, Cremonese, 1953, vol. 2, pp. 201–217, and (in English) in Hubert Kennedy, Selected Works of Giuseppe Peano, Toronto University Press, 1973, pp 190–205.

[Plo77]

Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[Rob66]

Abraham Robinson. Non-standard Analysis. North-Holland, 1966. Revised edition, 1996, published by Princeton University Press.

[Rog92]

Hartley Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, third edition, 1992.

[Ros01]

Frank Rosemeier. A constructive approach to Conway’s theory of games. In Peter Schuster, Ulrich Berger, and Horst Osswald, editors, Reuniting the Antipodes: Constructive and Nonstandard Views of the Continuum. Springer-Verlag, 2001.

[Sch03]

Peter Schuster. Unique existence, approximate solutions and countable choice. Theoretical Computer Science, 305:433–455, 2003.

[Sch05]

Peter Schuster. What is continuity, constructively? Journal of Universal Computer Science, 11(12):2076–85, 2005.

[Sco72a]

Dana S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, number 274 in Lecture Notes in Mathematics, pages 97–136. Springer-Verlag, Berlin, 1972.

[Sco72b]

Dana S. Scott. Lattice theory, data types and semantics. In Randall Rustin, editor, Formal Semantics of Programming Languages. Prentice-Hall, 1972.

[Spi10]

Bas Spitters. Located and overt sublocales. Annals of Pure and Applied Logic, 2010. to appear.

[Ste85]

David Stevenson. Binary floating-point arithmetic. ANSI/IEEE Standard, 754, 1985. Revised, 2008.

[Sto83]

Otto Stolz. Zur Geometrie der Alten, insbesondere über ein Axiom des Archimedes. Mathematische Annalen, 22(4):504–519, 1883.

[Str80]

Ross Street. Cosmoi of internal categories. Transactions of the American Mathematical Society, 258:271–318, 1980.

[SW78]

Ross Street and Robert Walters. Yoneda structures on 2-categories. Journal of Algebra, 50:350–379, 1978.

[Tay91]

Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[Tay99]

Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[Tho80]

Walter Tholen. A note on total categories. Bulletin of the Australian Mathematical Society, 21:169–173, 1980.

[TvD88]

Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in Mathematics, an Introduction. Number 121 and 123 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1988.

[Ver94]

Japie J. C. Vermeulen. Proper maps of locales. Journal of Pure and Applied Algebra, 92:79–107, 1994.

[Waa05]

Frank Waaldijk. On the foundations of constructive mathematics – especially in relation to the theory of continuous functions. Foundations of Science, 10(3):249–324, 2005.

[Wei00]

Klaus Weihrauch. Computable Analysis. Springer, Berlin, 2000.

[Woo82]

Richard J. Wood. Some remarks on total categories. Journal of Algebra, 75:538–545, 1982.

The papers on abstract Stone duality may be obtained from

[O]

Paul Taylor, Foundations for Computable Topology. in Giovanni Sommaruga (ed.), Foundational Theories of Mathematics, Kluwer 2010.

[A]

Paul Taylor, Sober spaces and continuations. Theory and Applications of Categories, 10(12):248–299, 2002.

[B]

Paul Taylor, Subspaces in abstract Stone duality. Theory and Applications of Categories, 10(13):300–366, 2002.

[C]

Paul Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284–338, 2000.

[D]

Paul Taylor, Non-Artin gluing in recursion theory and lifting in abstract Stone duality. 2000.

[E]

Paul Taylor, Inside every model of Abstract Stone Duality lies an Arithmetic Universe. Electronic Notes in Theoretical Computer Science 122 (2005) 247-296.

[F]

Paul Taylor, Scott domains in abstract Stone duality. March 2002.

[G–]

Paul Taylor, Local compactness and the Baire category theorem in abstract Stone duality. Electronic Notes in Theoretical Computer Science 69, Elsevier, 2003.

[G]

Paul Taylor, Computably based locally compact spaces. Logical Methods in Computer Science, 2 (2006) 1–70.

[H–]

Paul Taylor, An elementary theory of the category of locally compact locales. APPSEM Workshop, Nottingham, March 2003.

[H]

Paul Taylor, An elementary theory of various categories of spaces and locales. November 2004.

[I]

Andrej Bauer and Paul Taylor, The Dedekind reals in abstract Stone duality. Mathematical Structures in Computer Science, 19 (2009) 757–838.

[J]

Paul Taylor, A λ-calculus for real analysis. Journal of Logic and Analysis, 2(5), 1–115 (2010)

[K]

Paul Taylor, Interval analysis without intervals. February 2006.

[L]

Paul Taylor, Tychonov’s theorem in abstract Stone duality. September 2004.

[M]

Paul Taylor, Cartesian closed categories with subspaces. 2009.

[N]

Paul Taylor, Computability in locally compact spaces. 2010.

This paper results from a collaboration that began with Paul Taylor’s visit to Ljubljana in November 2004. A preliminary version of this work was presented at Computability and Complexity in Analysis in Kyoto on 28 August 2005, and we are grateful to Peter Hertling and the CCA programme committee for the indulgence of allowing us to occupy altogether 80 pages of their proceedings. We would also like to thank Vasco Brattka, Douglas Bridges, Thierry Coquand, Fer-Jan de Vries, Peter Johnstone, Vladek Kreinovich, Russell O’Connor, Andrea Schalk, Peter Schuster, Alex Simpson, Bas Spitters, Chris Stone, Maarten van Emden and Graham White for their helpful comments, and the anonymous referee for a most professional report.

Correspondence (by email only, please):
Andrej Bauer, Department of Mathematics and Physics, University of Ljubljana.
Paul Taylor.
Andrej.Bauer@andrej.com     pt08@PaulTaylor.EU