A constructive proof of the Heine-Borel covering theorem for formal reals

1. P. Aczel. An Introduction to Inductive Definitions, in Handbook of Mathematical Logic, J. Barwise ed., North-Holland (1977) 739–782.

   Google Scholar 

2. L. E. J. Brouwer. Die intuitionistische Form des Heine-Borelschen Theorems, in L. E. J. Brouwer Collected Works, A. Heyting ed., North-Holland, Amsterdam (1975) vol. 1, 350–351, 1926C.

   Google Scholar 

3. E. Bishop. “Foundations of Constructive Analysis”, Mc Graw Hill, 1967.

   Google Scholar 

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

5. J. Cederquist, T. Coquand, S. Negri Helly-Hahn-Banach in formal topology, forthcoming.

   Google Scholar 

6. T. Coquand. An intuitionistic proof of Tychonoff 's theorem, The Journal of Symbolic Logic vol. 57, no. 1 (1992) 28–32.

   Google Scholar 

7. T. Coquand. Constructive Topology and Combinatorics, proceeding of the conference Constructivity in Computer Science, San Antonio, LNCS 613 (1992) 159–164.

   Google Scholar 

8. M. P. Fourman, R.J. Grayson. Formal Spaces, in “The L. E. J. Brouwer Centenary Symposium”, A. S. Troelstra and D. van Dalen (eds), North-Holland, Amsterdam (1982) 107–122.

   Google Scholar 

9. M. Franchella. “L. E. J. Brouwer pensatore eterodosso. L'intuizionismo tra matematica e filosofia”, Guerini Studio (1994).

   Google Scholar 

10. A. Heyting. “Intuitionism, an introduction”, North-Holland (1971).

    Google Scholar 

11. P. T. Johnstone. “Stone Spaces”, Cambridge University Press (1982).

    Google Scholar 

12. L. Magnusson, “The Implementation of ALF — a Proof Editor based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution”, Chalmers University of Technology and University of Göteborg, PhD thesis (1995).

    Google Scholar 

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

    Google Scholar 

14. P. Martin-Löf. “Intuitionistic type theory”, notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Bibliopolis, Napoli (1984).

    Google Scholar 

15. S. Negri. Stone bases, alias the constructive content of Stone representation, “Logic and Algebra”, A. Ursini and P. Aglianò eds., Dekker, New York (1996) 617–636.

    Google Scholar 

16. S. Negri. “Dalla topologia formale all'analisi”, Ph.D. thesis, University of Padua (1996).

    Google Scholar 

17. S. Negri, D. Soravia. The continuum as a formal space, Rapporto Interno n.4, 17-7-95, Dipartimento di Matematica Pura e Applicata, Universitá di Padova.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

20. G. Sambin. Intuitionistic formal spaces — a first communication, in Mathematical logic and its applications, D. Skordev ed., Plenum (1987) 187–204.

    Google Scholar 

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

    Google Scholar 

22. G. Sambin, S. Valentini, P. Virgili. Constructive Domain Theory as a branch of Intuitionistic Pointfree Topology, Theoretical Computer Science (in press).

    Google Scholar 

23. W. P. van Stigt. “Brouwer's Intuitionism”, Studies in the History and Philosophy of Mathematics, vol. 2, North-Holland (1990).

    Google Scholar 

Download references