{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T12:03:12Z","timestamp":1648900992162},"reference-count":31,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3674,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1016\/s0304-3975(02)00699-0","type":"journal-article","created":{"date-parts":[[2003,4,25]],"date-time":"2003-04-25T10:09:04Z","timestamp":1051265344000},"page":"85-109","source":"Crossref","is-referenced-by-count":5,"title":["Constructive metrisability in point-free topology"],"prefix":"10.1016","volume":"305","author":[{"given":"Giovanni","family":"Curi","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(02)00699-0_BIB1","series-title":"Logic Colloquium \u201977","first-page":"55","article-title":"The type-theoretic interpretation of constructive set theory","author":"Aczel","year":"1979"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1002\/mana.19901490107","article-title":"Compactification of frames","volume":"149","author":"Banaschewski","year":"1990","journal-title":"Math. Nachr."},{"issue":"1","key":"10.1016\/S0304-3975(02)00699-0_BIB3","first-page":"167","article-title":"A new look at point-free metrisation theorems","volume":"39","author":"Banaschewski","year":"1998","journal-title":"Comment. Math. Univ. Carolin."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB4","series-title":"Constructive Analysis","author":"Bishop","year":"1985"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB5","doi-asserted-by":"crossref","unstructured":"C. Burden, C. Mulvey, Banach Spaces in Categories of Sheaves, Lecture Notes in Mathematics, Vol. 753, Springer, Berlin, 1979, pp. 169\u2013196.","DOI":"10.1007\/BFb0061818"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB6","doi-asserted-by":"crossref","unstructured":"J. Cederquist, T. Coquand, S. Negri, The Hahn\u2013Banach theorem in Type Theory, in: G. Sambin, J. Smith (Eds.), Twenty-Five Years of Constructive Type Theory, Proc. Cong., Venice, October 1995, Oxford University Press, Oxford, 1998, pp. 57\u201372.","DOI":"10.1093\/oso\/9780198501275.003.0006"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB7","unstructured":"T. Coquand, Formal compact Hausdorff spaces, unpublished."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB8","doi-asserted-by":"crossref","unstructured":"T. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic., to appear.","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB9","unstructured":"G. Curi, Analisi costruttiva nella teoria dei tipi: topologie formali con diametro e distanza, Degree Thesis, Universit\u00e0 di Padova, 1998."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB10","doi-asserted-by":"crossref","unstructured":"G. Curi, The points of (locally) compact regular formal topologies, in: U. Berger, H. Osswald, P.M. Schuster (Eds.), Reuniting the Antipodes\u2014Constructive and Nonstandard Views of the Continuum, Synth\u00e8se Library, Vol. 306, Proc. Symp. San Servolo Venice, Italy, 1999, Kluwer Academic Publishers, Dordrecht, 2001, pp. 39\u201354.","DOI":"10.1007\/978-94-015-9757-9_4"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB11","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/S0022-4049(99)00172-3","article-title":"The regular-locally-compact coreflection of a stably locally compact locale","volume":"157","author":"Escard\u00f2","year":"2001","journal-title":"J. Pure Appl. Algebra"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB12","series-title":"The L.E.J. Brouwer Centenary Symp","first-page":"107","article-title":"Formal Spaces","author":"Fourman","year":"1982"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB13","doi-asserted-by":"crossref","first-page":"5","DOI":"10.7146\/math.scand.a-11409","article-title":"Atomless part of space","volume":"31","author":"Isbell","year":"1972","journal-title":"Math. Scand."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB14","series-title":"Stone Spaces","author":"Johnstone","year":"1982"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB15","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1090\/conm\/030\/749770","article-title":"Open locales and exponentiation","volume":"30","author":"Johnstone","year":"1984","journal-title":"Contemp. Math."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB16","unstructured":"D. Lacombe, Quelques proc\u00e9d\u00e9s de d\u00e9finitions en topologie recursif, in: A. Heyting (Ed.), Constructivity in Mathematics, North-Holland, Amsterdam, 1959, pp. 129\u2013158."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB17","series-title":"Notes on Constructive Mathematics","author":"Martin-L\u00f6f","year":"1970"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB18","unstructured":"P. Martin-L\u00f6f, Intuitionistic Type Theory, Lecture Notes by Giovanni Sambin, Studies in Proof Theory, Bibliopolis, Napoli, 1984."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0001-8708(91)90082-I","article-title":"A globalization of the Hahn\u2013Banach theorem","volume":"89","author":"Mulvey","year":"1991","journal-title":"Adv. in Math."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB20","series-title":"Proc. Types Meeting, Aussois, 1996","first-page":"333","article-title":"Continuous lattices in formal topology","volume":"Vol. 1512","author":"Negri","year":"1998"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB21","series-title":"Programming in Martin-L\u00f6f's Type Theory","author":"Nordstrom","year":"1990"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB22","first-page":"91","article-title":"Pointless uniformities I. Complete regularity","volume":"25","author":"Pultr","year":"1984","journal-title":"Comm. Math. Univ. Carolinae"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB23","first-page":"105","article-title":"Pointless uniformities II. (Dia)metrisation","volume":"25","author":"Pultr","year":"1984","journal-title":"Comm. Math. Univ. Carolinae"},{"issue":"Suppl. 6","key":"10.1016\/S0304-3975(02)00699-0_BIB24","first-page":"247","article-title":"Remarks on metrisable locales, Proc. 12th Winter School on Abstract Analysis (Srnm, 1984)","volume":"2","author":"Pultr","year":"1984","journal-title":"Rend. Circ. Mat. Palermo"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB25","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1017\/S0305004100067773","article-title":"Categories of diametric frames","volume":"105","author":"Pultr","year":"1989","journal-title":"Mat. Proc. Cambridge Philos Soc."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB26","series-title":"Mathematical Logic and its Applications","first-page":"187","article-title":"Intuitionistic formal spaces\u2014a first communication","author":"Sambin","year":"1987"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB27","doi-asserted-by":"crossref","unstructured":"G. Sambin, Some points in formal topology, Theoret. Comput. Sci., this volume.","DOI":"10.1016\/S0304-3975(02)00704-1"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB28","doi-asserted-by":"crossref","unstructured":"G. Sambin, S. Valentini, Building up a toolbox for Martin-L\u00f6f's type theory: subset theory, in: G. Sambin, J. Smith (Eds.), Twenty-Five years of Constructive Type Theory, Proc. Cong., Venice, October 1995, Oxford University Press, Oxford, 1998, pp. 221\u2013244.","DOI":"10.1093\/oso\/9780198501275.003.0014"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB29","doi-asserted-by":"crossref","unstructured":"D.S. Scott, Continuous lattices, in: Toposes, Algebraic Geometry, and Logic, Lecture Notes in Mathematics, Vol. 274, Springer, Berlin, 1972, pp. 97\u2013136.","DOI":"10.1007\/BFb0073967"},{"key":"10.1016\/S0304-3975(02)00699-0_BIB30","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0304-3975(77)90045-7","article-title":"Effectively given domains","volume":"5","author":"Smyth","year":"1977","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(02)00699-0_BIB31","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/0304-3975(81)90027-X","article-title":"Embedding metric spaces into cpo's","volume":"16","author":"Weihrauch","year":"1981","journal-title":"Theoret. Comput. Sci."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502006990?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502006990?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,6,6]],"date-time":"2021-06-06T21:14:27Z","timestamp":1623014067000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397502006990"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":31,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["S0304397502006990"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(02)00699-0","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}