Some points in formal topology.
type: Item
instance of: scholarly article
title: Some points in formal topology.
zbMATH Open document ID: 1044.54001
DOI: 10.1016/S0304-3975(02)00704-1
author: Giovanni Sambin
published in: Theoretical Computer Science
publication date: 2004-03-14T00:00:00Z
review text: It is now more than fifteen years since the appearance of the author's `first communication' on formal spaces, a constructive and predicative approach to general topology designed to be interpretable in Martin-Löf's type theory. The present paper has three main aims, which are developed in three broadly independent sections: first, to survey the progress that has been made since then in developing traditional notions of topology in the formal setting; secondly, to provide publicity for what the author calls `the basic picture', which is a newer and more symmetric way of looking at the relationship between points and open sets, still under development by the author and S.~Gebellato; and finally, in a section less mathematical and more philosophical in character, to present the author's understanding of how and why one should seek to develop mathematics in a constructive context.
Mathematics Subject Classification ID: 54A05
Mathematics Subject Classification ID: 03A05
Mathematics Subject Classification ID: 03F65
zbMATH DE Number: 2055980
reviewed by: Peter Johnstone
MaRDI profile type: Publication
cites work: Q4843177
cites work: Pretopologies and a uniform presentation of sup-lattices, quantales and frames
cites work: Q5573965
cites work: Errett Bishop: Reflections on him and his research
cites work: Q4944905
cites work: Q4247301
cites work: An intuitionistic proof of Tychonoff's theorem
cites work: Formal topologies on the set of first-order formulae
cites work: Inductively generated formal topologies.
cites work: Q4513577
cites work: Q4552734
cites work: Constructive metrisability in point-free topology.
cites work: Q5540221
cites work: Q3322099
cites work: Q4944859
cites work: Linear logic
cites work: Q3965241
cites work: Q3226265
cites work: Q4944857
cites work: Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
cites work: Q5181669
cites work: Q3328540
cites work: The continuum as a formal space
cites work: Tychonoff's theorem in the framework of formal topologies
cites work: Q3999860
cites work: Computer science today. Recent trends and developments
cites work: Q3481701
cites work: Pretopologies and completeness proofs
cites work: Q4513593
cites work: Finitary formal topologies and Stone's representation theorem
cites work: Q4247310
cites work: Constructive domain theory as a branch of intuitionistic pointfree topology
cites work: Q3959414
cites work: Formal spaces and their effective presentations
cites work: Q4023900
cites work: Q4247312
cites work: A cartesian closed category in Martin-Löf's intuitionistic type theory
cites work: Q3994458
cites work: Embedding metric spaces into CPO's
full work available at URL: s0304-3975(02)00704-1
OpenAlex ID: W2076232585
description: scientific article; zbMATH DE number 2055980