home | mathematics | formal topology | some developments ::... 1 | 2

- A treatment of real numbers in which the computational content is preserved: the first reference is Numeri reali e analisi costruttiva nel contesto delle topologie formali, laurea thesis by D. Soravia, 1996

- Inductive (see Inductively generated formal topologies by T. Coquand et al.) and coinductive definitions (see Generating positivity by coinduction by P. Martin-Löf and myself in the BP book.

- The technological problem of implementing mathematics on a computer: see Toolbox and Toward a minimalist foundation...

- Foundations and proof theory put to practice: interaction between the foundations of mathematics and the actual development of mathematics, methods from proof theory in the practice of mathematics, logical nature of topological definitions, etc.

The particularly natural way in which this variety of aspects coexists in formal topology makes the approach at the same time coherent and flexible, and justifies hopes for a further rich development.