Abstract
A representation of continuous and prime-continuous lattices via formal topology is found. This representation stems from special examples of formal topologies in constructive analysis that give rise to the definition of the classes of locally Stone and locally Scott formal topologies. As an application, a representation theorem for locally compact spaces is obtained.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky, A. Jung. Domain theory, in “Handbook of Logic in Computer Science”, vol. 3, Clarendon Press, Oxford, pp. 1–168, 1994.
P. Aczel. An introduction to inductive definitions, in “Handbook of Mathematical Logic”, J. Barwise (ed), North-Holland, pp. 739–782, 1977.
B. Banaschewski, R.-E. Hoffmann (eds), “Continuous Lattices”, Lecture Notes in Mathematics 871, pp. 209–248, Springer, 1981.
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.
J. Cederquist. A machine assisted formalization of pointfree topology in type theory, Chalmers University of Technology and University of Göteborg, Sweden, Licentiate Thesis, 1994.
J. Cederquist. An implementation of the Heine-Borel covering theorem in type theory, this volume.
J. Cederquist. A machine assisted proof of the Hahn-Banach theorem, Chalmers University of Technology and University of Göteborg, 1997.
J. Cederquist, T. Coquand, S. Negri. The Hahn-Banach theorem in type theory, to appear in “Twenty-Five Years of Constructive Type Theory” G. Sambin and J. Smith (eds), Oxford University Press.
J. Cederquist, S. Negri. A constructive proof of the Heine-Borel covering theorem for formal reals, in “Types for Proofs and Programs”, S. Berardi and M. Coppo (eds), Lecture Notes in Computer Science 1158, pp. 62–75, Springer, 1996.
A. Edalat. Domain theory and integration, Theoretical Computer Science 151, pp. 163–193, 1995.
A. Edalat, S. Negri. The generalized Riemann integral on locally compact spaces (extended abstract), in “Advances in Theory and Formal Methods of Computing” A. Edalat, S. Jourdan and G. McCusker (eds), World Scientific, Singapore, 1996.
A. Edalat, S. Negri. The generalized Riemann integral on locally compact spaces, Topology and its Applications (in press).
M. P. Fourman, R.J. Grayson. Formal spaces, in “The L. E. J. Brouwer Centenary Symposium”, A. S. Troelstra and D. van Dalen (eds), pp. 107–122, North-Holland, Amsterdam, 1982.
G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove, D. S. Scott. “A Compendium on Continuous Lattices”, Springer, 1980.
K.H. Hoffmann, J.D. Lawson. The spectral theory of distributive continuous lattices. Transactions of the American Mathematical Society 246, pp. 285–310, 1978.
K.H. Hoffmann, M.W. Mislove. Local compactness and continuous lattices, in “Continuous Lattices”, B. Banaschewski and R.-E. Hoffmann (eds), op. cit..
J.R. Isbell. Atomless parts of spaces, Mathematica Scandinavica 31, pp. 5–32, 1972.
P. T. Johnstone. “Stone Spaces”, Cambridge University Press, 1982.
A. Joyal, M. Tierney. An extension of the Galois theory of Grothendieck, Memoirs of the American Mathematical Society 51, no. 309, pp. 1–71, 1984.
S. MacLane. “Categories for the Working Mathematician”, Springer, 1971.
P. Martin-Löf. “Notes on Constructive Mathematics”, Almqvist & Wiksell, Stockholm, 1970.
P. Martin-Löf. “Intuitionistic Type Theory”, Bibliopolis, Napoli, 1984.
C.J. Mulvey, J.W. Pelletier. A globalization of the Hahn-Banach theorem, Advances in Mathematics 89, pp. 1–60, 1991.
S. Negri. Stone bases, alias the constructive content of Stone representation, in “Logic and Algebra”, A. Ursini and P. Aglianó, (eds), Dekker, New York, pp. 617–636, 1996.
S. Negri. “Dalla topologia formale all'analisi”, Ph. D. thesis, University of Padova, 1996.
S. Negri, D. Soravia. The continuum as a formal space, Archive for Mathematical Logic (in press).
S. Negri, S. Valentini. Tychonoff's theorem in the framework of formal topologies, The Journal of Symbolic Logic (in press).
B. Nordström, K. Petersson, J. Smith, “Programming in Martin-Löf's Type Theory”, Oxford University Press, 1990.
G. Sambin. Intuitionistic formal spaces—a first communication, in “Mathematical Logic and its Applications”, D. Skordev (ed), Plenum Press, New York, pp. 187–204, 1987.
G. Sambin. Intuitionistic formal spaces and their neighbourhood, in “Logic Colloquium '88”, R. Ferro et al., (eds), pp. 261–285, North-Holland, Amsterdam, 1989.
G. Sambin, S. Valentini, P. Virgili. Constructive domain theory as a branch of intuitionistic pointfree topology, Theoretical Computer Science 159, pp. 319–341, 1996.
D.S. Scott. Continuous lattices, in “Toposes, Algebraic Geometry and Logic”, F.W. Lawvere (ed), Lecture Notes in Mathematics 274, pp. 97–136, Springer, 1972.
D.S. Scott. Models for various type-free calculi, in “Logic, Methodology and Philosophy of Science IV”, P. Suppes et al. (eds), North-Holland, pp. 157–187, 1973.
I. Sigstam. “On formal spaces and their effective presentations”, Ph. D. thesis, Report 1990:7, Department of Mathematics, University of Uppsala.
I. Sigstam. Formal spaces and their effective presentation, Archive for Mathematical Logic 34, pp. 211–246, 1995.
I. Sigstam, V. Stoltenberg-Hansen. Representability of locally compact spaces by domains and formal spaces, Theoretical Computer Science 179, pp. 319–331, 1997.
V. Stoltenberg-Hansen, I. Lindström, E.R. Griffor. “Mathematical Theory of Domains”, Cambridge University Press, 1994.
S. Vickers. “Topology via Logic”, Cambridge University Press, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Negri, S. (1998). Continuous lattices in formal topology. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097800
Download citation
DOI: https://doi.org/10.1007/BFb0097800
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65137-6
Online ISBN: 978-3-540-49562-8
eBook Packages: Springer Book Archive