References

[AAB80]

Ahmad Abd-Allah and Ronald Brown. A compact-open topology on partial maps with open domain. Journal of the London Mathematical Society (2), 21:480–6, 1980.

[Acz80]

Peter Aczel. Frege structures and the notions of proposition, truth and set. In J. Barwise, H. J. Keisler, and K. Kunen, editors, The Kleene Symposium, pages 31–59. North-Holland Publishing Company, 1980.

[Acz88]

Peter Aczel. Non-well-founded sets. Number 14 in Lecture Notes. Center for the Study of Language and Information, 1988.

[Acz94]

Peter Aczel. Final universes of processes. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, number 802 in Lecture Notes in Computer Science, pages 1–28. Springer Verlag, 1994.

[AGV64]

Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, editors. Séminaire de Géometrie Algébrique, IV: Théorie des Topos, number 269–270 in Lecture Notes in Mathematics. Springer-Verlag, 1964. Second edition, 1972.

[AH83]

Götz Alefeld and Jürgen Herzberger. Introduction to Interval Computations. Academic Press, 1983.

[AM89]

Peter Aczel and Paul Mendler. A final coalgebra theorem. In Proceedings of the 1989 Summer Conference on Category Theory and Computer Science, number 389 in Lecture Notes in Computer Science, pages 357–365. Springer Verlag, 1989.

[App92]

Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

[Bai85]

Günter Baigger. Die Nichtkonstruktivität des Brouwerschen Fixpunktsatzes. Archiv für Mathematische Logik und Grundlagenforschung, 25(3-4):183–188, 1985.

[Bar79]

Michael Barr. *-Autonomous Categories. Number 752 in Lecture Notes in Mathematics. Springer-Verlag, 1979.

[Bar81]

Henk Barendregt. The Lambda Calculus: its Syntax and Semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, 1981. Second edition, 1984.

[Bar88]

Robert Barnhart. Chambers Dictionary of Etymology. 1988.

[Bar92]

Henk Barendregt. Lambda calculi with types. In Samson Abramsky et al., editors, Handbook of Logic in Computer Science, volume 2, pages 117–309. Oxford University Press, 1992.

[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.

[BB78]

Peter Booth and Ronald Brown. Spaces of partial maps, fibred mapping spaces and the compact-open topology. General Topology and its Applications, 8:181–195, 1978.

[BB85]

Errett A. Bishop and Douglas S. Bridges. Constructive Analysis. Number 279 in Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1985.

[BB08]

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.

[BBS04]

Andrej Bauer, Lars Birkedal, and Dana S. Scott. Equilogical spaces. Theoretical Computer Science, 315:35–59, 2004.

[Ber78]

Gérard Berry. Stable models of typed λ-calculi. In ICALP, Lecture Notes in Computer Science, pages 72–89. Springer-Verlag, 1978.

[Ber90]

Ulrich Berger. Totale Objekte und Mengen in der Bereichstheorie. PhD thesis, Mathematisches Institut der Universität München, 1990.

[Bet90]

Rodolfo Bettazzi. Teoria della Grandezza. Pisa, 1890.

[BFS03]

Anna Bucalo, Carsten Führmann, and Alex Simpson. An equational notion of lifting monad. TCS, 2003.

[BGvO71]

Michael Barr, Pierre Grillet, and Donovan van Osdol, editors. Exact Categories and Categories of Sheaves. Number 236 in Lecture Notes in Mathematics. Springer-Verlag, 1971.

[Bis67]

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

[BIS02]

Douglas S. Bridges, Hajime Ishihara, and Peter Schuster. Compactness and continuity, constructively revisited. In Julian Bradfield, editor, Computer Science Logic, number 2471 in Lecture Notes in Computer Science, pages 89–102. Springer-Verlag, 2002.

[BK08]

Andrej Bauer and Iztok Kavkler. Implementing real numbers with RZ. Electronic Notes in Theoretical Computer Science, 202:365–384, 2008.

[Bol17]

Bernhard P. J. N. Bolzano. Rein analytischer Beweis des Lehrsatzes, dass zwischen je zwey Werthen, die ein entgegengesetztes resultat gewähren, wenigstens eine reelle Wurzel der Gleichen liege. 1817. English translation by Steve Russ in Historia Mathematica 7 (1980), 156–185 and The Mathematical Works of Bernhard Bolzano, Oxford University Press, 2004, pages 253–277.

[Bou57]

Nicolas Bourbaki. Eléments de Mathématique XXII: Théories des Ensembles, Livre I, Structures. Number 1258 in Actualités scientifiques et industrielles. Hermann, 1957. English translation, “Theory of Sets,” 1968.

[Bou66]

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

[BP80]

Michael Barr and Robert Paré. Molecular toposes. Journal of Pure and Applied Algebra, 17:127–132, 1980.

[BR87]

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

[BR97]

A. Bucalo and Giuseppe Rosolini. Lifting. In E. Moggi and Giuseppe Rosolini, editors, Category Theory and Computer Science, volume 1290 of Lectures Notes in Computer Science, pages 281–292, S. Margherita Ligure, 1997.

[BR98a]

Anna Bucalo and Giuseppe Rosolini. Repleteness and the associated sheaf. Journal of Pure and Applied Algebra, 127:147–151, 1998.

[BR98b]

Anna Bucalo and Giuseppe Rosolini. Repleteness and the associated sheaf. Journal of Pure and Applied Algebra, 127:147–151, 1998.

[Bri99]

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

[Bro12a]

L. E. J. Brouwer. Invarianz des n-dimensionalen Gebiets. Mathematischen Annalen, 71:305–313, 1912.

[Bro12b]

L. E. J. Brouwer. Über Abbildung von Mannigfaltigkeiten. Mathematischen Annalen, 71:97–115, 1912.

[Bro64]

Ronald Brown. Function spaces and product topologies. Quarterly Journal of Mathematics, 15(1):238–250, 1964.

[Bro75]

Jan Brouwer. Collected Works: Philosophy and Foundations of Mathematics, volume 1. North-Holland, 1975. Edited by Arend Heyting.

[Bro88]

Ronald Brown. Topology: a Geometric Account of General Topology, Homotopy Types and the Fundamental Groupoid. Mathematics and its Applications. Ellis Horwood, 1988. First edition “Elements of modern topology,” 1968.

[BS08]

Andrej Bauer and Christopher Stone. RZ: a tool for bringing constructive and computable mathematics closer to programming practice. Journal of Logic and Computation, 19:17–43, 2008.

[BW85]

Michael Barr and Charles Wells. Toposes, Triples, and Theories. Springer-Verlag, Berlin, Germany, Heidelberg, Germany, London, UK etc., 1985.

[BY]

Vasco Brattka and Atsushi Yoshikawa. Towards computability of elliptic boundary value problems in variational formulation. Journal of Complexity.

[Cau21]

Augustin-Louis Cauchy. Cours d’Analyse de l’école royale polytechnique, première partie: Analyse algébrique. 1821. Œvres complètes, série 2, tome 3.

[CG92]

Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type checking in f_≤. Mathematical Structures in Computer Science, 2:55–91, 1992.

[CH06]

Felice Cardone and J. Roger Hindley. History of lambda-calculus and combinatory logic. Handbook of the History of Logic, 5, 2006.

[Cle87]

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

[CLW93a]

Aurelio Carboni, Steve Lack, and Robert Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84:145–158, 1993.

[CLW93b]

Aurelio Carboni, Steve Lack, and Robert F. C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84:145–158, 1993.

[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.

[Coc90]

J. Robin Cockett. List-arithmetic distributive categories: Locoi. Journal of Pure and Applied Algebra, 66:1–29, 1990.

[Coc93]

J. Robin B. Cockett. Introduction to distributive categories. Mathematical Structures in Computer Science, 3:277–307, 1993.

[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.

[Cor03]

David Corfield. Towards a Philosophy of Real Mathematics. Cambridge University Press, 2003.

[CPR91]

Aurelio Carboni, Maria-Cristina Pedicchio, and Giuseppe Rosolini, editors. Proceedings of the 1990 Como Category Conference, number 1488 in Lecture Notes in Mathematics. Springer-Verlag, 1991.

[CR36]

Alonzo Church and J. Barkley Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 39(3):472–482, 1936.

[CS88]

John Horton Conway and Neil Sloane. Sphere Packings, Lattices and Groups. Number 290 in Grundlehren der Mathematischen Wissenschaften. Springer-Verlag, 1988.

[CUV06]

Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inf. & Comp., 204:437–468, 2006.

[CW87]

Aurelio Carboni and Robert Walters. Cartesian bicategories. I. Journal of Pure and Applied Algebra, 49(1–2):11–32, 1987.

[Dau79]

Joseph Warren Dauben. Georg Cantor: his Mathematics and Philosophy of the Infinite. Harvard University Press, 1979.

[Dav65]

Martin Davis. The Undecidable. Basic Papers on Undecidable, Unsolvable Problems and Computable Functions. Raven Press, Hewlett, N.Y., 1965.

[Dav05a]

E. Brian Davies. A defence of mathematical pluralism. Philosophia Mathematica, 13(3):252–276, 2005.

[Dav05b]

E. Brian Davies. Pluralism in mathematics. Philosophical Transactions of the Royal Society, A 363:2449–60, 2005.

[Day72]

Brian Day. A reflection theorem for closed categories. Journal of Pure and Applied Algebra, 2:1–1, 1972.

[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 Øystein Ore; republished by Chelsea, New York, 1969.

[DG03]

James Dugundji and Andrzej Granas. Fixed Point Theory. Springer Verlag, 2003.

[Die77]

Jean Alexandre Dieudonné. Panorama des Mathématiques Pures: la Choix Bourbachique. Gauthier-Villars, 1977. English translation, “A panorama of pure mathematics, as seen by N. Bourbaki” by I. G. Macdonald, Academic Press, Pure and Applied Mathematics, 97, 1982.

[Dij76]

Edsger Dijkstra. A Discipline of Programming. Prentice–Hall, 1976.

[Dij87]

E. J. Dijksterhuis. Archimedes. Princeton University Press, 1987. Written in Dutch in 1938–44; translated by C. Dikshoorn.

[DK70]

Brian Day and Max Kelly. On topological quotient maps preserved by pullbacks or products. Mathematical Proceedings of the Cambridge Philosophical Society, 67:553–8, 1970.

[dP89]

Valeria de Paiva. A dialectica-like model of linear logic. Lecture Notes In Computer Science, pages 341–356, 1989.

[DP90]

Brian Davey and Hilary Priestley. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press, Cambridge, U.K., 1990.

[dP91]

Valeria de Paiva. The Dialectica Categories. PhD thesis, University of Cambridge Computer Laboratory, 1991.

[dPS99]

Valeria de Paiva and Andrea Schalk. Building models for linear logic. In Proc. of the 7th Conference on Algebraic Methodology and Soft ware Technology (AMAST ’98), number 1548 in Lecture Notes in Computer Science, pages 164–177. Springer-Verlag, 1999.

[DT87]

Roy Dyckhoff and Walter Tholen. Exponentiable maps, partial products and pullback complements. Journal of Pure and Applied Algebra, 49:103–116, 1987.

[Dug66]

James Dugundji. Topology. Allyn and Bacon, 1966.

[Eck69]

Beno Eckmann, editor. Number 80 in Lecture Notes in Mathematics. Springer-Verlag, 1969.

[EE96]

Abbas Edalat and Martín Hötzel Escardó. Integration in real PCF. 1996.

[Ehr06]

Philip Ehrlich. The rise of non-Archimedean mathematics and the roots of a misconception I: The emergence of non-Archimedean systems of magnitudes. Archive for History of Exact Sciences, 60(1):1–121, 2006.

[EJ92]

Jean-Claude Evard and Farhad Jafari. A complex Rolle’s theorem. American Mathematical Monthly, 99:858–869, 1992.

[EL04]

Abbas Edalat and André Lieutier. Domain theory and differential calculus. Mathematical Structures in Computer Science, 14(6):771–802, 2004.

[EM65]

Samuel Eilenberg and John C. Moore. Adjoint functors and triples. Illinois Journal of Mathematics, 9:381–98, 1965.

[ES98]

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

[ES01]

Martín Escardó and Alex Simpson. A universal characterisation of the closed Euclidean interval. 2001.

[Esc99]

Martín Escardó. On the compact regular coreflection of a stable compact locale. In Proceedings of the 15th conference on Mathematical Foundations of Programming Semantics (MFPS XV), volume 20 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.

[Esc04]

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

[Fak70]

Sabah Fakir. Monade idempotente associée à une monade. Comptes Rendues de l’Academie des Sciences de Paris, Série A–B, 270:A99–101, 1970.

[Fef77]

Solomon Feferman. Categorical foundations and foundations of category theory. In R. Butts and J. Hintikka, editors, Logic, Foundations of Mathematics and Computability Theory, pages 149–169. Reidel, 1977.

[FG87]

John Fauvel and Jeremy Gray. The History of Mathematics, a Reader. Macmillan and the Open University, 1987.

[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.

[Fis93]

Michael Fischer. Lambda-calculus schemata. Lisp and Symbolic Computation, 6:259–288, 1993.

[FMRS92]

Peter Freyd, Philip Mulry, Giuseppe Rosolini, and Dana Scott. Extensional PERs. Information and Computation, 98:211–227, 1992. See Logic in Computer Science 5 for an extended abstract.

[Fox45]

Ralph H. Fox. On topologies for function-spaces. Bulletin of the American Mathematical Society, 51, 1945.

[FR97a]

Marcelo Fiore and Giuseppe Rosolini. The category of cpos from a synthetic point of view. Electronic Notes in Theoretical Computer Science, 6, 1997.

[FR97b]

Marcelo Fiore and Giuseppe Rosolini. Two models of synthetic domain theory. Journal of Pure and Applied Algebra, 116:151–162, 1997.

[Fre93]

Gottlob Frege. Grundgesetze der Arithmetik. 1893. English translation, The Basic Laws of Arithmetic, by Montgomery Furth, University of California Press, 1964.

[Fre66a]

Peter Freyd. Algebra-valued functors in general and tensor products in particular. Colloq. Math., 14:89–106, 1966.

[Fre66b]

Peter J. Freyd. The theory of functors and models. In Theory of Models — Proceedings of the 1963 International Symposium at Berkeley, pages 107–120. North Holland, 1966.

[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.

[FS90]

Peter Freyd and Andre Scedrov. Categories, Allegories, volume 39 of North-Holland Mathematical Library. North-Holland, Amsterdam, 1990.

[Füh99]

Carsten Führmann. Direct models of the computational lambda-calculus. In Mathematical Foundations of Programming Semantics 15, number 20 in Electronic Notes in Theoretical Computer Science, 1999.

[Füh02]

Carsten Führmann. Varieties of effects. In Proceedings FOSSACS 2002, number 2303 in Lecture Notes in Computer Science, pages 144–158. Springer-Verlag, 2002.

[FW90]

Barry Fawcett and Richard Wood. Completely distributive lattices I. Mathematical Proceedings of the Cambridge Philosophical Society, 107:81–9, 1990.

[GD71]

Alexander Grothendieck and Jean Alexandre Dieudonné. Eléments de Géometrie Algébrique, tome I: le Langage des Schémas. Number 166 in Grundlehren der mathematische Wissenschaften. Springer-Verlag, 1971. Originally published by IHES in 1960.

[GDRT05]

Alexandre Goldsztejn, David Daney, Michel Rueher, and Patrick Taillibert. Modal intervals revisited: a mean-value extension to generalized intervals. In Quantification in Constraint Programming, 2005.

[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.

[GG00]

Ivor Grattan-Guinness, editor. The Search for Mathematical Roots, 1870–1940. Princeton University Press, 2000.

[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.

[Gir72]

Jean Giraud. Classifying topos. In Bill Lawvere, editor, Toposes, Algebraic Geometry, and Logic, number 274 in Lecture Notes in Mathematics, pages 43–56. Springer-Verlag, 1972.

[Gir87]

Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[GLT89]

Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Göd31]

Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931. English translations, “On Formally Undecidable Propositions of ‘Principia Mathematica’ and Related Systems” published by Oliver and Boyd, 1962 and Dover, 1992; also in “From Frege to Gödel: a Source Book in Mathematical Logic, 1879–1931”, ed. Jan van Heijenoort, Harvard University Press, 1967.

[GS06]

Gary Gruenhage and Thomas Streicher. Quotients of countably based spaces are not closed under sobrification. Mathematical Structures in Computer Science, 16:223–229, 2006.

[Hak72]

Monique Hakim. Topos Annelés et Schémas Relatifs. Number 64 in Ergebnisse der Mathematik und ihre Grenzgebiete. Springer-Verlag, 1972.

[Han69]

Eldon Hansen. Topics in Interval Analysis. Oxford University Press, 1969.

[Har08]

G. H. Hardy. A Course of Pure Mathematics. Cambridge University Press, 1908. Tenth edition, 1952, frequently reprinted.

[Har77]

Robin Hartshorne. Algebraic Geometry. Number 52 in Graduate Texts in Mathematics. Springer-Verlag, 1977.

[Hau14]

Felix Hausdorff. Grundzüge der Mengenlehre. 1914. Chapters 7–9 of the first edition contain the material on topology, which was removed from later editions. Reprinted by Chelsea, 1949 and 1965; there is apparently no English translation.

[Hay87]

Christopher Haynes. Logic continuations. Journal of Logic Programming, 4:157–176, 1987.

[Hec06]

Reinhold Heckmann. A cartesian closed extension of the category of locales. Mathematical Structures in Computer Science, 16(02):231–253, 2006.

[Hey56]

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

[HHPJW07]

Paul Hudak, John Hughes, Simon Peyton-Jones, and Philip Wadler. A history of Haskell: Being lazy with class. In History of Programming Languages, pages 12–55. ACM Press, 2007.

[HL78]

Karl Hofmann and Jimmie Lawson. The spectral theory of distributive continuous lattices. Transactions of the American Mathematical Society, 246:285–310, 1978.

[HLPZ]

Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, and Paul Zimmermann. The MPFR Library. INRIA. www.mpfr.org.

[HM81]

Karl H. Hofmann and Michael Mislove. Local compactness and continuous lattices. In Bernhard Banaschewski and Rudolf-Eberhard Hoffmann, editors, Continuous Lattices, number 871 in Springer Lecture Notes in Mathematics, pages 209–248, 1981.

[Hof95]

Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, University of Edinburgh, 1995.

[Höl01]

Otto Hölder. Die Axiome der Quantität und die Lehre vom Mass. Ber. Verh. Sachs. Wiss. Leipzig, Math.-Phis. C, 1:1–64, 1901. Partial English translation, "The axioms of quantity and the theory of measurement...", by Joel Michell and Catherine Ernst, in J. Math. Psychology, 41:345–356, 1997.

[How80]

William A. Howard. The formulae-as-types notion of construction. In Haskell Curry, Jonathan Seldin, and Roger Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.

[HP89]

J. Martin E. Hyland and Andrew M. Pitts. The theory of constructions: Categorical semantics and topos-theoretic models. In John Gray and Andre Scedrov, editors, Proceedings of the Boulder Conference on Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 137–199, Providence, Rhode Island, 1989. American Mathematical Society.

[HR90]

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

[HS99]

J. Martin E. Hyland and Andrea Schalk. Abstract games for linear logic. ENTCS, 29, 1999. CTCS 1999.

[HS02]

J. Martin E. Hyland and Andrea Schalk. Games on graphs and sequentially realizable functionals. In Logic in Computer Science. IEEE Computer Science Press, 2002. LiCS 2002.

[HS03]

J. Martin E. Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, 294:183–231, 2003.

[Hud89]

Paul Hudak. Conception, evolution, and application of functional programming languages. ACM Computing Surveys, 21(3):411, 1989.

[Hyl79]

J. Martin E. Hyland. Filter spaces and continuous functionals. Annals of Mathematical Logic, 16:101–143, 1979.

[Hyl81]

J. Martin E. Hyland. Function spaces in the category of locales. In Bernhard Banachewski and Rudolf-Eberhard Hoffman, editors, Continuous Lattices, number 871 in LNM, pages 264–281. Springer-Verlag, 1981.

[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.

[Hyl88]

J. Martin E. Hyland. A small complete category. Annals of Pure and Applied Logic, 40(2):135–165, November 1988.

[Hyl91]

J. Martin E. Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria-Cristina Pedicchio, and Giuseppe Rosolini, editors, Proceedings of the 1990 Como Category Conference, number 1488 in Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[Isb75a]

John Isbell. Function spaces and adjoints. Math Scand, 36:317–39, 1975.

[Isb75b]

John Isbell. Meet-continuous lattices. Symposia Math, 16:41–54, 1975.

[Isb82]

John Isbell. Completion of a construction of Johnstone. Proceedings of the American Mathematical Society, 85:333–4, 1982.

[Isb86]

John Isbell. General function spaces, products and continuous lattices. Mathematical Proceedings of the Cambridge Philosophical Society, 100(2):193–205, 1986.

[Jib98]

Mamuka Jibladze. Lower bagdomain as a glueing. Proc. Razmadze Math. Inst., 118:31–41, 1998.

[JKDW01]

Luc Jaulin, Michel Kieffer, Olivier Didrit, and Eric Walter. Applied Interval Analysis. Springer, 2001.

[JKM99]

Achim Jung, Mathias Kegelmann, and Andrew Moshier. Multi lingual sequent calculus and coherent spaces. Fundamenta Informaticae, 37(4):369–412, 1999.

[JKM01]

Achim Jung, Mathias Kegelmann, and Andrew Moshier. Stably compact spaces and closed relations. Electronic Notes in Theoretical Computer Science, 45, 2001.

[JM95]

André Joyal and Ieke Moerdijk. Algebraic Set Theory. Number 220 in London Mathematical Society Lecture Notes in Mathematics. Cambridge University Press, 1995.

[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.

[Joh85]

Peter T. Johnstone. Vietoris locales and localic semi-lattices. In R.-E. Hoffmann and K. H. Hofmann, editors, Continuous Lattices and their Applications, number 101 in Pure and Applied Mathematics, pages 155–180. Marcel Dekker, 1985.

[Joh91]

Peter T. Johnstone. Partial products, bagdomains and hyperlocal toposes. In Michael Fourman, Peter Johnstone, and Andrew Pitts, editors, Applications of Categories in Computer Science, volume 177 of LMS Lecture Note Series, pages 315–339. Cambridge University Press, 1991.

[Joy73]

André Joyal. Arithmetic universes and Gödel’s incompleteness theorem. Manuscript, 1973.

[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.

[JS96]

Achim Jung and Philipp Sünderhauf. On the duality of compact vs. open. In S. Andima, R. C. Flagg, G. Itzkowitz, P. Misra, Y. Kong, and R. D. Kopperman, editors, Papers on general topology and applications: Eleventh Summer Conference at University of Southern Maine, volume 806 of Annals of the New York Academy of Sciences, pages 214–230, 1996.

[JT84]

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

[Jun90]

Achim Jung. The classification of continuous domains. In Logic in Computer Science, pages 35–40. IEEE Computer Society Press, 1990.

[JV91]

Peter T. Johnstone and Steven J. Vickers. Preframe presentations present. In Aurelio Carboni, Cristina Pedicchio, and Giuseppe Rosolini, editors, Category Theory — Proceedings, Como, 1990, number 1488 in Lecture Notes in Mathematics, pages 193–212. Springer Verlag, 1991.

[JW93]

Luc Jaulin and Eric Walter. Set inversion via interval analysis for nonlinear bounded-error estimation. Automatica, 29:1053–64, 1993.

[Kag99]

Alexander Kaganovsky. Exact Computing in Positional Weighted Systems. PhD thesis, University of Kent, 1999.

[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.

[Kel55]

John Kelley. General Topology. Van Nostrand, 1955. Reprinted by Springer-Verlag, Graduate Texts in Mathematics, 27, 1975.

[Kel86]

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

[Kil85]

Wilhelm Killing. Die nicht-Euklidischen Raumformen in Analytischer Behandlung. BG Teubner, 1885.

[Kle45]

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

[KM74]

Anders Kock and Christian Mikkelsen. Non-standard extensions in the theory of toposes. In Albert Hurd and Peter Loeb, editors, Victoria Symposium on Nonstandard Analysis, number 369 in Lecture Notes in Mathematics, pages 122–143. Springer-Verlag, 1974.

[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.

[Koc95]

Anders Kock. Monads for which structures are adjoint to units. Journal of Pure and Applied Algebra, 104:41–59, 1995.

[KP93]

Max Kelly and John Power. Adjunctions whose counits are coequalisers. Journal of Pure and Applied Algebra, 89:163–179, 1993.

[Kuh62]

Thomas S Kuhn. The Structure of Scientific Revolutions. University of Chicago Press, 1962.

[Kur20]

Kazimierz Kuratowski. Sur la notion d’ensemble fini. Fundamenta Mathematicae, 1:130–1, 1920.

[KW96]

Wiesaw Krawcewicz and Jianhong Wu. Theory of Degrees, with Application to Bifurcations and Differential Equations. Wiley, 1996.

[Lak63]

Imre Lakatos. Proofs and refutations: the logic of mathematical discovery. British Journal for the Philosophy of Science, 14:1–25, 1963. Re-published by Cambridge University Press, 1976, edited by John Worrall and Elie Zahar.

[Lak95]

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

[Lam07]

Branimir Lambov. RealLib: An efficient implementation of exact real arithmetic. Mathematical Structures in Computer Science, 17(1):81–98, 2007. www.brics.dk/∼barnie/RealLib/.

[Lan64]

Peter Landin. The mechanical evaluation of expressions. Computer Journal, 6, 1964.

[Law64]

Bill Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences of the United States of America, 52:1506–1511, 1964.

[Law69]

Bill Lawvere. Adjointness in foundations. Dialectica, 23:281–296, 1969. Reprinted with commentary in Theory and Applications of Categories Reprints, 16:1–16, 2006.

[Law70]

Bill Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In Alex Heller, editor, Applications of Categorical Algebra, number 17 in Proceedings of Symposia in Pure Mathematics, pages 1–14. American Mathematical Society, 1970.

[Law71]

Bill Lawvere. Quantifiers and sheaves. In Actes du Congrès International des Mathématiciens, volume 1, pages 329–334. Gauthier-Villars, 1971.

[Law80]

F. William Lawvere. Toward the description in a smooth topos of the dynamically possible motions and deformations of a continuous body. Cahiers de Topologie et Géometrie Différentielle, 21:377–92, 1980.

[Law00]

Bill Lawvere. Comments on the development of topos theory. In Jean-Paul Pier, editor, Development of Mathematics, 1950–2000. Birkhäuser, 2000.

[Lin69]

Fred Linton. An outline of functorial semantics. In Beno Eckmann, editor, Seminar on Triples and Categorical Homology Theory, number 80 in Lecture Notes in Mathematics, pages 7–52. Springer-Verlag, 1969.

[Llo78]

Noel Lloyd. Degree Theory. Number 73 in Cambridge Tracts in Mathematics. Cambridge University Press, 1978.

[LR73]

Joachim Lambek and Basil Rattray. Localizations at injective objects in complete categories. Proceedings of the American Mathematical Society, 41:1–9, 1973.

[LR75]

Joachim Lambek and Basil Rattray. Localizations and sheaf reflectors. Transactions of the American Mathematical Society, 210:275–293, 1975.

[LS86]

Joachim Lambek and Philip Scott. Introduction to Higher-Order Categorical Logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, Cambridge, U.K, 1986. First paperback edition (with corrections) 1988.

[Mac71]

Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, Berlin, 1971.

[Mai03]

Marie Emilia Maietti. Joyal’s arithmetic universes via type theory. Electronic Notes in Theoretical Computer Science, 69, 2003.

[Mai05]

Marie Emilia Maietti. Reflection into models of finite decidable FP-sketches in an arithmetic universe. Electronic Notes in Theoretical Computer Science, 416, 2005.

[Man76]

Ernie Manes. Algebraic Theories. Number 26 in Graduate Texts in Mathematics. Springer-Verlag, 1976.

[Man83]

Mark Mandelkern. Constructive continuity. Memoirs of the American Mathematical Society, 42(277), 1983.

[Mar47]

Andrei Markov. On the representation of recursive functions. Dokl. Akad. Nauk SSSR, 58:1891–2, 1947.

[McC78]

John McCarthy. History of LISP. History of programming languages, pages 173–185, 1978.

[McL90]

Colin McLarty. The uses and abuses of the history of topos theory. British Journal for the Philosophy of Science, 41(3):351–375, 1990.

[Mik76]

Christian Mikkelsen. Lattice-theoretic and Logical Aspects of Elementary Topoi. PhD thesis, Århus Universitet, 1976. Various publications, number 25.

[Mil97]

John W. Milnor. Topology from the Differentiable Viewpoint. Princeton University Press, 1997.

[ML63]

Saunders Mac Lane. Natural associativity and commutativity. Rice University Studies, 49(4):28–46, 1963.

[ML75]

Per Martin-Löf. An intuitionistic theory of types: Predicative part. In Harvey Rose and John Sheperdson, editors, Logic Colloquium ’73, number 80 in Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, 1975.

[ML84]

Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.

[ML88]

Saunders Mac Lane. Categories and concepts in perspective. In Peter Duren, Richard A. Askey, and Uta C. Merzbach, editors, A Century of Mathematics in America, volume 1, pages 323–365. American Mathematical Society, 1988. Addendum in volume 3, pages 439–441.

[ML98]

Per Martin-Löf. An intutionistic theory of types. In Giovanni Sambin and Jan Smith, editors, Twenty-Five Years of Constructive Type Theory, number 36 in Oxford Logic Guides. Oxford University Press, 1998.

[Mog88]

Eugenio Moggi. Computational lambda-calculus and monads. Technical report, LFCS, University of Edinburgh, 1988.

[Mog91]

Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[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.

[MR77]

Michael Makkai and Gonzalo Reyes. First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories. Number 611 in Lecture Notes in Mathematics. Springer-Verlag, 1977.

[MR97]

Michael Makkai and Giuseppe Rosolini. Studying repleteness in the category of cpos. Electronic Notes in Theoretical Computer Science, 6, 1997.

[MRW02]

Francisco Marmolejo, Robert Rosebrugh, and Richard Wood. A basic distributive law. Journal of Pure and Applied Algebra, 168:209–226, 2002.

[MS03]

Matías Menni and Alex Simpson. Topological and limit-space subcategories of countably-based equilogical spaces. Mathematical Structures in Computer Science, 12(6):739–770, 2003.

[Mül96]

Norbert Müller. Towards a real Real RAM: a prototype using C++. In Ker-I Ko, Norbert Müller, and Klaus Weihrauch, editors, Computability and Complexity in Analysis. Universität Trier, 1996. Second CCA Workshop, Trier, August 22–23, 1996; www.informatik.uni-trier.de/iRRAM.

[Mül01]

Norbert Müller. The iRRAM: Exact arithmetic in C++. In Jens Blanck, Vasco Brattka, and Peter Hertling, editors, Computability and Complexity in Analysis: 4th International Workshop, CCA 2000 Swansea, UK, September 17, 2000, Selected Papers, number 2064 in Lecture Notes in Computer Science. Springer-Verlag, 2001.

[Nac92]

Leopoldo Nachbin. Compact unions of closed subsets are closed and compact intersections of open subsets are open. Portugaliae Mathematica, 49:403–9, 1992.

[Ner59]

Anil Nerode. Some Stone spaces and recursion. Duke Mathematics Journal, 26:397, 1959.

[Neu90]

Arnold Neumaier. Interval Methods for Systems of Equations. Cambridge University Press, 1990.

[Nie82]

Susan Niefield. Cartesianness: Topological spaces, uniform spaces and affine varieties. Journal of Pure and Applied Algebra, 23:147–167, 1982.

[Nor99]

Dag Normann. The continuous functionals. In Griffor E. R., editor, Handbook of Computability Theory, chapter 8, pages 251–275. North Holland, 1999.

[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.

[Par71]

Robert Paré. On absolute colimits. Journal of Algebra, 19:80–95, 1971.

[Par74]

Robert Paré. Colimits in topoi. Bulletin of the American Mathematical Society, 80(3):556–561, May 1974.

[Pas65]

Boris Pasynkov. Partial topological products. Transactions of the Moscow Mathematical Society, 13:153–271, 1965.

[Pau96]

Lawrence Paulson. ML for the Working Programmer. CUP, 1996. Second edition.

[Pea89]

Giuseppe Peano. Arithmetices Principia, Nova Methodo Exposita. Fratres Bocca, Turin, 1889. English translation, The Principles of Arithmetic, presented by a new method, in [vH67a], pages 20–55.

[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.

[Pét53]

H. Pétard. A contribution to the mathematical theory of big game hunting. Eureka, 16, 1953. Reprinted in Lion hunting and other mathematical pursuits by Ralph Boas, Gerald Alexanderson and Dale Mugler, Mathematical Association of America, 1995.

[Pho90a]

Wesley Phoa. Domain Theory in Realizability Toposes. PhD thesis, University of Cambridge, 1990. University of Edinburgh Dept. of Computer Science report CST-82-91 and ECS-LFCS-91-171.

[Pho90b]

Wesley Phoa. Effective domains and intrinsic structure. In Logic in Computer Science 5, pages 366–377. IEEE Computer Society Press, 1990.

[Pit01]

Andrew M. Pitts. Categorical logic. In Handbook of Logic in Computer Science, volume 5, pages 39–128. Oxford University Press, 2001.

[Plo75]

Gordon D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1:125–159, 1975.

[Plo77]

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

[Pot07]

Petrus H. Potgieter. Computable counter-examples to the Brouwer fixed-point theorem. arXiv:0804.3199, 2007.

[Pow84]

John Power. Butler’s Theorems. PhD thesis, McGill University, 1984.

[Pow02]

John Power. Premonoidal categories as categories with algebraic structure. Theoretical Computer Science, 278:303–321, 2002.

[PR97]

John Power and Edmund Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7:453–468, 1997.

[Pre05]

Matija Pretnar. Sintentivcna topologija. BSc thesis, 2005.

[PT89]

Andrew Pitts and Paul Taylor. A note on Russell’s Paradox in locally cartesian closed categories. Studia Logica, 48:377–387, 1989.

[PW99]

Cristina Pedicchio and Richard Wood. Groupoidal completely distributive lattices. Journal of Pure and Applied Algebra, 1999. Barr volume.

[RB88]

David Rydeheard and Rod Burstall. Computational Category Theory. Prentice Hall, 1988.

[Rey93]

John Reynolds. The discoveries of continuations. Lisp and Symbolic Computation, 6:233–247, 1993.

[Ric54]

Henry Rice. Recursive real numbers. Proceedings of the American Mathematical Society, 5:784–791, 1954.

[Ric56a]

Henry Rice. Recursive and recursively enumerable orders. Transactions of the American Mathematical Society, 83:277, 1956.

[Ric56b]

Henry G. Rice. On completely recursively enumerable classes and their key arrays. Journal of Symbolic Logic, 21:304–8, 1956.

[Ric98]

Fred Richman. Generalized real numbers in constructive mathematics. Indagationes Mathematicae, 9:595–606, 1998.

[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.

[Ros86]

Giuseppe Rosolini. Continuity and Effectiveness in Topoi. D. phil. thesis, University of Oxford, 1986.

[Ros90]

Giuseppe Rosolini. About modest sets. International Journal on the Foundations of Computer Science, 1:341–353, 1990.

[Ros94]

Giuseppe Rosolini. Notes on synthetic domain theory. ftp.disi.unige.it, 1994.

[Ros00]

Giuseppe Rosolini. Equilogical spaces and filter spaces. Rendiconti del Circolo Matematico di Palermo, Supplemento, 64:157–175, 2000.

[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.

[RR88a]

Edmund Robinson and Giuseppe Rosolini. Categories of partial maps. Inform. and Comput., 79(2):95–130, November 1988.

[RR88b]

Edmund Robinson and Giuseppe Rosolini. Categories of partial maps. Information and Computation, 79:95–130, 1988.

[RR90]

Eedmund Robinson and Giuseppe Rosolini. Colimit completions and the effective topos. Journal of Symbolic Logic, 55:678–699, 1990.

[RT98]

Giuseppe Rosolini and Paul Taylor. Abstract stone duality in synthetic domain theory. In preparation, 1998.

[Rus05]

Bertrand Russell. On denoting. Mind, 14:479–93, 1905.

[RW13]

Bertrand Russell and Alfred North Whitehead. Principia Mathematica. Cambridge University Press, 1910–13.

[RW91]

Robert Rosebrugh and Richard Wood. Completely distributive lattices II. Mathematical Proceedings of the Cambridge Philosophical Society, 110:245–9, 1991.

[RW94]

Robert Rosebrugh and Richard Wood. Completely distributive lattices IV. App. Cat. Str., 2:119–144, 1994.

[Sam87]

Giovanni Sambin. Intuitionistic formal spaces: a first communication. In D. Skordev, editor, Mathematical Logic and its Applications, pages 187–204. Plenum, 1987.

[Sam03]

Giovani Sambin. Some points in formal topology. Th. Comp. Sci., 305:347–408, 2003.

[Sar93]

Vijay A. Saraswat. Concurrent Constraint Programming. MIT Press, 1993.

[Sch93]

Andrea Schalk. Domains arising as algebras for power space monads. Journal of Pure and Applied Algebra, 89:305–328, 1993.

[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.

[Sco66]

Dana Scott. More on the axiom of extensionality. In Yehoshua Bar-Hillel, E. I. J. Poznanski, M. O. Rabin, and Abraham Robinson, editors, Essays of the Foundations of Mathematics, pages 115–139. Magnes Press, Hebrew University, 1966. Distributed by Oxford University Press.

[Sco70]

Dana Scott. Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Sciences and Systems, pages 169–176, 1970. Superseded by Oxford technical report PRG-2.

[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.

[Sco76]

Dana Scott. Data types as lattices. SIAM Journal on Computing, 5:522–587, 1976.

[Sco82]

Dana Scott. Domains for denotational semantics. In M. Nielson and E. M. Schmidt, editors, Automata, Languages and Programming: Proceedings 1982, number 140 in Lecture Notes in Computer Science. Springer-Verlag, 1982.

[Sco93]

Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121:422–440, 1993. Written in 1969.

[SdP02]

Andrea Schalk and Valeria de Paiva. Poset-valued sets, or, how to build models for linear logic. Theoretical Computer Science, 2002.

[Sel01]

Peter Selinger. Control categories and duality. MSCS, 11:207–260, 2001.

[Sel02]

Jonathan P. Seldin. Curry’s anticipation of the types used in programming languages. Proceedings of the Canadian Society for History and Philosophy of Mathematics, 15:148–163, 2002.

[Sim78]

Harold Simmons. The lattice-theoretic part of topological separation properties. Proceedings of the Edinburgh Mathematical Society (2), 21(1):41–48, 1978.

[Sim82]

Harold Simmons. A couple of triples. Topology Appl, 13:201–23, 1982.

[Smo06]

Lee Smolin. The Trouble with Physics. Houghton Mifflin, 2006. Republished by Penguin, 2008.

[Smy77]

Michael Smyth. Effectively given domains. Theoretical Computer Science, 5:257–274, 1977.

[Smy83]

Michael Smyth. Powerdomains and predicate transformers: a topological view. In Josep Díaz, editor, Automata, Languages and Programming, number 154 in Lecture Notes in Computer Science, pages 662–675. Springer-Verlag, 1983.

[Smy94]

Michael Smyth. Topology. In Samson Abramsky et al., editors, Handbook of Logic in Computer Science, volume 1, pages 641–761. Oxford University Press, 1994.

[Spe28]

Emanuel Sperner. Neuer Beweis für die Ivarianz der Dimensionzahl und des Gebietes. Abh. Math. Sem. Hamburg, V:265–272, 1928.

[Spi10]

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

[SS70]

J. Arthur Seebach and Lynn Arthur Steen. Counterexamples in Topology. Holt, Rinehart and Winston, 1970. Republished by Springer-Verlag, 1978 and by Dover, 1995.

[Ste67]

Norman Steenrod. A convenient category of topological spaces. Michigan Mathematics Journal, 14(2):133–152, 1967.

[Ste78]

Guy Steele. Rabbit: A compiler for Scheme. Technical Report AI TR 474, MIT, May 1978.

[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.

[Sto37]

Marshall H. Stone. Applications of the theory of Boolean rings to general topology. Transactions of the American Mathematical Society, 41(3):375–481, 1937.

[Sto38]

Marshall H. Stone. The representation of Boolean algebras. Bulletin of the American Mathematical Society, 44(12):807–816, 1938.

[Str80]

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

[Str84]

Ross Street. The family approach to total cocompleteness and toposes. Transactions of the American Mathematical Society, 284:355–369, 1984.

[SW74]

Christopher Strachey and Christopher Wadsworth. Continuations: a mathematical semantics for handling full jumps. Technical Report PRG-11, Oxford University Computing Laboratory, 1974.

[SW78]

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

[Tar35]

Alfred Tarski. Zur Grundlegung der Boole’schen algebra. Fundamenta Mathematicae, 24:177–198, 1935.

[Tay83]

Paul Taylor. Applications of continuous lattices to λ-calculus and denotational semantics. Master’s thesis, University of Cambridge, May 1983.

[Tay86a]

Paul Taylor. Internal completeness of categories of domains. In David Pitt, editor, Category Theory and Computer Programming I (Guildford, September 1985), volume 240 of Lecture Notes in Computer Science, pages 449–465. Springer Verlag, 1986.

[Tay86b]

Paul Taylor. Recursive Domains, Indexed category Theory and Polymorphism. PhD thesis, Cambridge University, 1986.

[Tay87]

Paul Taylor. Homomorphisms, bilimits and saturated domains — some very basic domain theory. 1987.

[Tay89]

Paul Taylor. Semantics of System F, volume 7 of Cambridge Tracts in Theoretical Computer Science, chapter appendix A, pages 131–148. Cambridge University Press, Cambridge, 1989.

[Tay90]

Paul Taylor. An algebraic approach to stable domains. Journal of Pure and Applied Algebra, 64:171–203, 1990.

[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.

[Tay96a]

Paul Taylor. Intuitionistic sets and ordinals. J. Symb. Logic, 61:705–744, 1996.

[Tay96b]

Paul Taylor. Towards a unified treatment of induction, I: The general recursion theorem. 1996.

[Tay99]

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

[Thi97a]

Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997.

[Thi97b]

Hayo Thielecke. Continuation semantics and self-adjointness. In Proceedings MFPS XIII, volume 6 of Electronic Notes in Theoretical Computer Science. Elsevier, 1997. URL: http://www.elsevier.nl/locate/entcs/volume6.html.

[Thi01]

Hayo Thielecke. Comparing control constructs by double-barrelled CPS transforms. In Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS17), Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001.

[Tho80]

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

[TP90]

Paul Taylor and Wesley Phoa. The synthetic Plotkin powerdomain. ftp://ftp.dcs.qmw.ac.uk/pub/lfp/pt/synpp.dvi, 1990.

[Tur35]

Alan M. Turing. On computable numbers with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society (2), 42:230–265, 1935.

[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.

[vD09]

Dirk van Dalen. Brouwer’s є-fixed point from Sperner’s lemma. 2009.

[Ver89]

Giuseppe Veronese. Il continuo rettilineo e l’assioma V di Archimede. Atti della Reale Accademia Dei Lincei, 6:603–624, 1889.

[Ver91]

Japie Vermeulen. Some constructive results related to compactness and the (strong) Hausdorff property for locales. In Carboni et al. [CPR91], pages 401–409.

[Ver94]

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

[vH67a]

Jan van Heijenoort, editor. From Frege to Gödel: a Source Book in Mathematical Logic, 1879–1931. Harvard University Press, 1967. Reprinted 1971, 1976.

[vH67b]

Jean van Heijenoort, editor. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Harvard University Press, 1967.

[vHDM97]

? van Hentenryck, ? Deville, and ? Michel. Numerica. MIT Press, 1997.

[Vic88]

Steven Vickers. Topology Via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1988.

[Vic95]

Steven Vickers. Locales are not pointless. In Chris Hankin, Ian Mackie, and Rajagopal Nagarajan, editors, Theory and Formal Methods of Computing 1994, 1995.

[Vic98]

Steven Vickers. Topical categories of domains. Mathematical Structures in Computer Science, 1998.

[Vic04a]

Steven Vickers. The double powerlocale and exponentiation. Theory and Applications of Categories, 12:372–422, 2004.

[Vic04b]

Steven Vickers. The double powerlocale and exponentiation: A case study in geometric logic. Theory and Applications of Categories, 12(13):372–422, 2004.

[vOS98]

Jaap van Oosten and Alex Simpson. Axioms and (counter)examples in synthetic domain theory. http://www.math.uu.nl/publications/preprints/1080.ps.gz, 1998.

[VT04]

SJ Vickers and CF Townsend. A universal characterization of the double powerlocale. Th. Comp. Sci., 316:297–321, 2004.

[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.

[Wil70]

Peter Wilker. Adjoint product and hom functors in general topology. Pacific Journal of Mathematics, 34:269–283, 1970.

[Wil94a]

Todd Wilson. The Assembly Tower and some Categorical and Algebraic Aspects of Frame Theory. PhD thesis, Carnegie–Mellon University, May 1994.

[Wil94b]

Todd Wilson. The Assembly Tower and some Categorical and Algebraic Aspects of Frame Theory. PhD thesis, Carnegie–Mellon University, 1994. CMU-CS-94-186.

[Win83]

G. Winskel. Powerdomains and modality. In M. Karpinski, editor, Foundations of Computation Theory, number 158 in Lecture Notes in Computer Science, pages 505–514, Berlin, 1983. Springer-Verlag.

[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.

The original inspiration for this work came during my visit to the Università degli Studi di Genova in March 1993. I would like to thank Martin Hyland, Fred Linton, Eugenio Moggi, Andy Pitts, Pino Rosolini, Andrea Schalk, Steve Vickers, Graham White and Richard Wood for their valuable comments.