Skip to main content

Continuous lattices in formal topology

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1512))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky, A. Jung. Domain theory, in “Handbook of Logic in Computer Science”, vol. 3, Clarendon Press, Oxford, pp. 1–168, 1994.

    Google Scholar 

  2. P. Aczel. An introduction to inductive definitions, in “Handbook of Mathematical Logic”, J. Barwise (ed), North-Holland, pp. 739–782, 1977.

    Google Scholar 

  3. B. Banaschewski, R.-E. Hoffmann (eds), “Continuous Lattices”, Lecture Notes in Mathematics 871, pp. 209–248, Springer, 1981.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  6. J. Cederquist. An implementation of the Heine-Borel covering theorem in type theory, this volume.

    Google Scholar 

  7. J. Cederquist. A machine assisted proof of the Hahn-Banach theorem, Chalmers University of Technology and University of Göteborg, 1997.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  10. A. Edalat. Domain theory and integration, Theoretical Computer Science 151, pp. 163–193, 1995.

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  12. A. Edalat, S. Negri. The generalized Riemann integral on locally compact spaces, Topology and its Applications (in press).

    Google Scholar 

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

    Google Scholar 

  14. G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove, D. S. Scott. “A Compendium on Continuous Lattices”, Springer, 1980.

    Google Scholar 

  15. K.H. Hoffmann, J.D. Lawson. The spectral theory of distributive continuous lattices. Transactions of the American Mathematical Society 246, pp. 285–310, 1978.

    Article  MathSciNet  Google Scholar 

  16. K.H. Hoffmann, M.W. Mislove. Local compactness and continuous lattices, in “Continuous Lattices”, B. Banaschewski and R.-E. Hoffmann (eds), op. cit..

    Google Scholar 

  17. J.R. Isbell. Atomless parts of spaces, Mathematica Scandinavica 31, pp. 5–32, 1972.

    MATH  MathSciNet  Google Scholar 

  18. P. T. Johnstone. “Stone Spaces”, Cambridge University Press, 1982.

    Google Scholar 

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

    MathSciNet  Google Scholar 

  20. S. MacLane. “Categories for the Working Mathematician”, Springer, 1971.

    Google Scholar 

  21. P. Martin-Löf. “Notes on Constructive Mathematics”, Almqvist & Wiksell, Stockholm, 1970.

    MATH  Google Scholar 

  22. P. Martin-Löf. “Intuitionistic Type Theory”, Bibliopolis, Napoli, 1984.

    Google Scholar 

  23. C.J. Mulvey, J.W. Pelletier. A globalization of the Hahn-Banach theorem, Advances in Mathematics 89, pp. 1–60, 1991.

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  25. S. Negri. “Dalla topologia formale all'analisi”, Ph. D. thesis, University of Padova, 1996.

    Google Scholar 

  26. S. Negri, D. Soravia. The continuum as a formal space, Archive for Mathematical Logic (in press).

    Google Scholar 

  27. S. Negri, S. Valentini. Tychonoff's theorem in the framework of formal topologies, The Journal of Symbolic Logic (in press).

    Google Scholar 

  28. B. Nordström, K. Petersson, J. Smith, “Programming in Martin-Löf's Type Theory”, Oxford University Press, 1990.

    Google Scholar 

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

    Google Scholar 

  30. G. Sambin. Intuitionistic formal spaces and their neighbourhood, in “Logic Colloquium '88”, R. Ferro et al., (eds), pp. 261–285, North-Holland, Amsterdam, 1989.

    Google Scholar 

  31. G. Sambin, S. Valentini, P. Virgili. Constructive domain theory as a branch of intuitionistic pointfree topology, Theoretical Computer Science 159, pp. 319–341, 1996.

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  34. I. Sigstam. “On formal spaces and their effective presentations”, Ph. D. thesis, Report 1990:7, Department of Mathematics, University of Uppsala.

    Google Scholar 

  35. I. Sigstam. Formal spaces and their effective presentation, Archive for Mathematical Logic 34, pp. 211–246, 1995.

    MATH  MathSciNet  Google Scholar 

  36. I. Sigstam, V. Stoltenberg-Hansen. Representability of locally compact spaces by domains and formal spaces, Theoretical Computer Science 179, pp. 319–331, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  37. V. Stoltenberg-Hansen, I. Lindström, E.R. Griffor. “Mathematical Theory of Domains”, Cambridge University Press, 1994.

    Google Scholar 

  38. S. Vickers. “Topology via Logic”, Cambridge University Press, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Eduardo Giménez Christine Paulin-Mohring

Rights and permissions

Reprints 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

Publish with us

Policies and ethics