{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:11Z","timestamp":1725474491841},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097800","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T09:27:48Z","timestamp":1164360468000},"page":"333-353","source":"Crossref","is-referenced-by-count":2,"title":["Continuous lattices in formal topology"],"prefix":"10.1007","author":[{"given":"Sara","family":"Negri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"18_CR1","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"S. Abramsky","year":"1994","unstructured":"S. Abramsky, A. Jung. Domain theory, in \u201cHandbook of Logic in Computer Science\u201d, vol. 3, Clarendon Press, Oxford, pp. 1\u2013168, 1994."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"P. Aczel. An introduction to inductive definitions, in \u201cHandbook of Mathematical Logic\u201d, J. Barwise (ed), North-Holland, pp. 739\u2013782, 1977.","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"B. Banaschewski, R.-E. Hoffmann (eds), \u201cContinuous Lattices\u201d, Lecture Notes in Mathematics 871, pp. 209\u2013248, Springer, 1981.","DOI":"10.1007\/BFb0089899"},{"key":"18_CR4","unstructured":"G. Battilotti, G. Sambin. A uniform presentation of sup-lattices, quantales and frames by means of infinitary preordered sets, pretopologies and formal topologies, Preprint no. 19, Dept. of Pure and Applied Mathematics, University of Padova, 1993."},{"key":"18_CR5","volume-title":"A machine assisted formalization of pointfree topology in type theory","author":"J. Cederquist","year":"1994","unstructured":"J. Cederquist. A machine assisted formalization of pointfree topology in type theory, Chalmers University of Technology and University of G\u00f6teborg, Sweden, Licentiate Thesis, 1994."},{"key":"18_CR6","unstructured":"J. Cederquist. An implementation of the Heine-Borel covering theorem in type theory, this volume."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"J. Cederquist. A machine assisted proof of the Hahn-Banach theorem, Chalmers University of Technology and University of G\u00f6teborg, 1997.","DOI":"10.1093\/oso\/9780198501275.003.0006"},{"key":"18_CR8","unstructured":"J. Cederquist, T. Coquand, S. Negri. The Hahn-Banach theorem in type theory, to appear in \u201cTwenty-Five Years of Constructive Type Theory\u201d G. Sambin and J. Smith (eds), Oxford University Press."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"J. Cederquist, S. Negri. A constructive proof of the Heine-Borel covering theorem for formal reals, in \u201cTypes for Proofs and Programs\u201d, S. Berardi and M. Coppo (eds), Lecture Notes in Computer Science 1158, pp. 62\u201375, Springer, 1996.","DOI":"10.1007\/3-540-61780-9_62"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/0304-3975(95)00050-7","volume":"151","author":"A. Edalat","year":"1995","unstructured":"A. Edalat. Domain theory and integration, Theoretical Computer Science 151, pp. 163\u2013193, 1995.","journal-title":"Theoretical Computer Science"},{"key":"18_CR11","doi-asserted-by":"crossref","DOI":"10.1142\/p028","volume-title":"Advances in Theory and Formal Methods of Computing","author":"A. Edalat","year":"1996","unstructured":"A. Edalat, S. Negri. The generalized Riemann integral on locally compact spaces (extended abstract), in \u201cAdvances in Theory and Formal Methods of Computing\u201d A. Edalat, S. Jourdan and G. McCusker (eds), World Scientific, Singapore, 1996."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"A. Edalat, S. Negri. The generalized Riemann integral on locally compact spaces, Topology and its Applications (in press).","DOI":"10.1016\/S0166-8641(97)00227-7"},{"key":"18_CR13","first-page":"107","volume-title":"The L. E. J. Brouwer Centenary Symposium","author":"M. P. Fourman","year":"1982","unstructured":"M. P. Fourman, R.J. Grayson. Formal spaces, in \u201cThe L. E. J. Brouwer Centenary Symposium\u201d, A. S. Troelstra and D. van Dalen (eds), pp. 107\u2013122, North-Holland, Amsterdam, 1982."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove, D. S. Scott. \u201cA Compendium on Continuous Lattices\u201d, Springer, 1980.","DOI":"10.1007\/978-3-642-67678-9"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2307\/1997975","volume":"246","author":"K.H. Hoffmann","year":"1978","unstructured":"K.H. Hoffmann, J.D. Lawson. The spectral theory of distributive continuous lattices. Transactions of the American Mathematical Society 246, pp. 285\u2013310, 1978.","journal-title":"Transactions of the American Mathematical Society"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"K.H. Hoffmann, M.W. Mislove. Local compactness and continuous lattices, in \u201cContinuous Lattices\u201d, B. Banaschewski and R.-E. Hoffmann (eds), op. cit..","DOI":"10.1007\/BFb0089908"},{"key":"18_CR17","doi-asserted-by":"crossref","first-page":"5","DOI":"10.7146\/math.scand.a-11409","volume":"31","author":"J.R. Isbell","year":"1972","unstructured":"J.R. Isbell. Atomless parts of spaces, Mathematica Scandinavica 31, pp. 5\u201332, 1972.","journal-title":"Mathematica Scandinavica"},{"key":"18_CR18","unstructured":"P. T. Johnstone. \u201cStone Spaces\u201d, Cambridge University Press, 1982."},{"issue":"no.309","key":"18_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/memo\/0309","volume":"51","author":"A. Joyal","year":"1984","unstructured":"A. Joyal, M. Tierney. An extension of the Galois theory of Grothendieck, Memoirs of the American Mathematical Society 51, no. 309, pp. 1\u201371, 1984.","journal-title":"Memoirs of the American Mathematical Society"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"S. MacLane. \u201cCategories for the Working Mathematician\u201d, Springer, 1971.","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"18_CR21","volume-title":"Notes on Constructive Mathematics","author":"P. Martin-L\u00f6f","year":"1970","unstructured":"P. Martin-L\u00f6f. \u201cNotes on Constructive Mathematics\u201d, Almqvist & Wiksell, Stockholm, 1970."},{"key":"18_CR22","unstructured":"P. Martin-L\u00f6f. \u201cIntuitionistic Type Theory\u201d, Bibliopolis, Napoli, 1984."},{"key":"18_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0001-8708(91)90082-I","volume":"89","author":"C.J. Mulvey","year":"1991","unstructured":"C.J. Mulvey, J.W. Pelletier. A globalization of the Hahn-Banach theorem, Advances in Mathematics 89, pp. 1\u201360, 1991.","journal-title":"Advances in Mathematics"},{"key":"18_CR24","first-page":"617","volume-title":"Logic and Algebra","author":"S. Negri","year":"1996","unstructured":"S. Negri. Stone bases, alias the constructive content of Stone representation, in \u201cLogic and Algebra\u201d, A. Ursini and P. Aglian\u00f3, (eds), Dekker, New York, pp. 617\u2013636, 1996."},{"key":"18_CR25","unstructured":"S. Negri. \u201cDalla topologia formale all'analisi\u201d, Ph. D. thesis, University of Padova, 1996."},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"S. Negri, D. Soravia. The continuum as a formal space, Archive for Mathematical Logic (in press).","DOI":"10.1007\/s001530050149"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"S. Negri, S. Valentini. Tychonoff's theorem in the framework of formal topologies, The Journal of Symbolic Logic (in press).","DOI":"10.2307\/2275645"},{"key":"18_CR28","unstructured":"B. Nordstr\u00f6m, K. Petersson, J. Smith, \u201cProgramming in Martin-L\u00f6f's Type Theory\u201d, Oxford University Press, 1990."},{"key":"18_CR29","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-1-4613-0897-3_12","volume-title":"Mathematical Logic and its Applications","author":"G. Sambin","year":"1987","unstructured":"G. Sambin. Intuitionistic formal spaces\u2014a first communication, in \u201cMathematical Logic and its Applications\u201d, D. Skordev (ed), Plenum Press, New York, pp. 187\u2013204, 1987."},{"key":"18_CR30","first-page":"261","volume-title":"Logic Colloquium '88","author":"G. Sambin","year":"1989","unstructured":"G. Sambin. Intuitionistic formal spaces and their neighbourhood, in \u201cLogic Colloquium '88\u201d, R. Ferro et al., (eds), pp. 261\u2013285, North-Holland, Amsterdam, 1989."},{"key":"18_CR31","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0304-3975(95)00169-7","volume":"159","author":"G. Sambin","year":"1996","unstructured":"G. Sambin, S. Valentini, P. Virgili. Constructive domain theory as a branch of intuitionistic pointfree topology, Theoretical Computer Science 159, pp. 319\u2013341, 1996.","journal-title":"Theoretical Computer Science"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"D.S. Scott. Continuous lattices, in \u201cToposes, Algebraic Geometry and Logic\u201d, F.W. Lawvere (ed), Lecture Notes in Mathematics 274, pp. 97\u2013136, Springer, 1972.","DOI":"10.1007\/BFb0073967"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"D.S. Scott. Models for various type-free calculi, in \u201cLogic, Methodology and Philosophy of Science IV\u201d, P. Suppes et al. (eds), North-Holland, pp. 157\u2013187, 1973.","DOI":"10.1016\/S0049-237X(09)70356-8"},{"key":"18_CR34","unstructured":"I. Sigstam. \u201cOn formal spaces and their effective presentations\u201d, Ph. D. thesis, Report 1990:7, Department of Mathematics, University of Uppsala."},{"key":"18_CR35","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF01469380","volume":"34","author":"I. Sigstam","year":"1995","unstructured":"I. Sigstam. Formal spaces and their effective presentation, Archive for Mathematical Logic 34, pp. 211\u2013246, 1995.","journal-title":"Archive for Mathematical Logic"},{"key":"18_CR36","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/S0304-3975(96)00152-1","volume":"179","author":"I. Sigstam","year":"1997","unstructured":"I. Sigstam, V. Stoltenberg-Hansen. Representability of locally compact spaces by domains and formal spaces, Theoretical Computer Science 179, pp. 319\u2013331, 1997.","journal-title":"Theoretical Computer Science"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"V. Stoltenberg-Hansen, I. Lindstr\u00f6m, E.R. Griffor. \u201cMathematical Theory of Domains\u201d, Cambridge University Press, 1994.","DOI":"10.1017\/CBO9781139166386"},{"key":"18_CR38","unstructured":"S. Vickers. \u201cTopology via Logic\u201d, Cambridge University Press, 1989."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097800","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,4]],"date-time":"2021-08-04T23:44:16Z","timestamp":1628120656000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097800"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/bfb0097800","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}