References

[Bau00]

Andrej Bauer.
The Realizability Approach to Computable Analysis and Topology.
PhD thesis, Carnegie Mellon University, 2000.
Available as CMU technical report CMUCS00164.
 [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 positivevalued uniformly continuous functions on
compact intervals.
New Zealand Journal of Mathematics, 38:129–135, 2008.
 [BB08b]

Josef Berger and Douglas S. Bridges.
The antiSpecker 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
SpringerVerlag (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. SpringerVerlag,
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 domaintheoretic 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. SpringerVerlag, 1979.
 [Fri58]

Richard Friedberg.
Un contreexample 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. NorthHolland,
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.
SpringerVerlag, 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. NorthHolland,
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.
SpringerVerlag, 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.
Nonstandard Analysis.
NorthHolland, 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. SpringerVerlag, 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.
SpringerVerlag, Berlin, 1972.
 [Sco72b]

Dana S. Scott.
Lattice theory, data types and semantics.
In Randall Rustin, editor, Formal Semantics of Programming
Languages. PrenticeHall, 1972.
 [Spi10]

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

David Stevenson.
Binary floatingpoint 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 2categories.
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. NorthHolland, 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, NonArtin 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) 247296.
 [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,
FerJan 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