Switch to: Citations

Add references

You must login to add references.
  1. Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
    Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...)
    Download  
     
    Export citation  
     
    Bookmark   44 citations  
  • The problem of the formalization of constructive topology.Silvio Valentini - 2005 - Archive for Mathematical Logic 44 (1):115-129.
    Abstract.Formal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in [CSSV]. However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Per Martin-Löf. Intuitionistic type theory. Studies in proof theory. Bibliopolis, Naples1984, ix + 91 pp. [REVIEW]W. A. Howard - 1986 - Journal of Symbolic Logic 51 (4):1075-1076.
    Download  
     
    Export citation  
     
    Bookmark   94 citations  
  • Formal spaces and their effective presentations.Inger Sigstam - 1995 - Archive for Mathematical Logic 34 (4):211-246.
    The theory of formal spaces is developed in terms of presentations, in order to study effectivity.
    Download  
     
    Export citation  
     
    Bookmark   7 citations