home | mathematics | formal topology | selection of my papers ::... 1 | 2

Formal topology: selection of my papers, with comments

(for full bibliographic data, see publications)

G. Sambin, Intuitionistic formal spaces - a first communication
The first paper on formal topologies and formal spaces. It contains definitions and most of the basic ideas, even if in a few pages.
A version in Latex, which includes the content of an addendum written in 1988, is Intuitionistic formal spaces.

G. Sambin, Pretopologies and completeness proofs
The definition of formal topology is generalized to that of pretopology, by suppressing the positivity predicate and by substituting covers with precovers. A cover becomes exactly the same as a precover satisfying the conditions corresponding to the structural rules of weakening and contraction.
A uniform, fully constructive (i.e. intuitionistic and predicative) proof of completeness is given for intuitionistic linear logic (without exponentials) and its extensions, including intuitionistic and classical logic.

G. Sambin - S. Valentini - P. Virgili, Constructive domain theory as a branch of intuitionistic pointfree topology, and G. Sambin, Formal topology and domains
The theme of these two papers is the connection between formal topology and domain theory. The first paper introduces the notion of information base, which becomes the bridge connecting Scott domains (the category of Scott domains is equivalent to that of information bases) with formal topologies (the category of information bases is equivalent to a subcategory of formal topologies, called Scott or unary formal topologies). The result is a very simple and natural new approach to the theory of domains. In the second paper, a definition of formal topology is introduced, in which formal intersection is not necessary; it is shown that unary formal topologies correspond precisely to algebraic cpo's.