Logic	FORMAL TOPOLOGY
Advanced course	GIOVANNI SAMBIN and SILVIO VALENTINI Department of Mathematics, Universitá di Padova
Both weeks	sambin@math.unipd.it and silvio@math.unipd.it
Course description	Formal Topology aims at the development of topology in a strictly constructive foundational theory, such as Martin-Lof's constructive type theory. Its general motivation is to bridge the gap between ordinary mathematics and computer languages. Type theory is itself a functional programming language. A toolbox on top of type theory is provided, which allows ordinary set-theoretic notation. The main definitions of topology are then expressed in such framework, which leads to the pointfree approach to topology in a natural way. The result is formal topology, which then is somehow similar to the present (impredicative) theory of locales. Its specific peculiarity is inductive definitions. The generality of definitions brings to several applications. Temptative contents of 10 ninety-minute lectures: Review of type theory and subsets Main definitions I: topological sytems and formal topologies Main definitions II: formal points, formal spaces, continuous functions Inductive generation of formal topologies Stone and Scott: what can be said constructively about Stone'srepresentation theory and Scott domains Predicative presentations and completeness theorems for intuitionistic linear logic and extensions The example of real numbers Extraction of a constructive proof of classical results The example of choice sequences More general notions of space and logic
Prerequisites	No prerequisite is strictly necessary for the main course, but obviously the lectures will be more fruitful for students aware of a little of topology (only the main definitions), type theory, inductive definitions, locale theory. For specific applications, something is assumed to be known, on representation of distributive lattices, sequent calculus, linear logic, etc.
Literature	No specific recommendation