Next: CNRS / Paris 7
Up: Cooperating sites
Previous: Université Paris-Sud


The logic research group in Padova has deep experience in using intuitionistic type theory for the development of mathematics, in particular formal topology. Its interest includes related matters such as normalization in type theories, connections with categorical universes, tools for user-friendly mathematical notation and proof search. This work has led also to basic logic, bringing a unified treatment to various constructive systems. The group has been active in TYPES since 1996, and organized the Second Workshop on Formal Topology in April 2002, a TYPES small workshop. The group has ongoing collaboration with the TYPES sites at Göteborg, München (LMU), Torino, Stockholm, Sophia Antipolis and Birmingham.

The group plans to contibute mainly to the Formal Mathematics objective of this proposal, with our work on formal topology, which we also plan to apply to computational mathematics and to theoretical computer science (e.g. models for concurrency). We also plan to organize the Third Workshop on Formal Topology in 2005 or 2006.

The senior members of the subsite are:

Padova homepage

Bengt Nordström 2005-09-22