Padova, October 2-4, 1997
organised by
the EC Types Working Group
Formal Topology offers a challenge to today's constructivist. It aims
at a theory of formal spaces, in some way similar to the present impredicative
theory of locales, but based on a more predicative constructive foundation
such as Martin-Löf's constructive type theory.
It has its historical roots in Brouwer's conception of the continuum
which he expressed in terms of choice sequences. The later analysis
and elimination of choice sequences led to connections between locale
theory and inductive definitions.
Formal Topology suggests techniques from the theory of locales for the extraction of constructive information from a priori non effective arguments. It also poses the challenge to develop an elegant constructive treatment of the standard notions of classical pointset topology - even the right approach to the notion of a `closed set' is at issue. Other topics include for instance sheaf models, applications outside topology itself, implementation problems, friendly `interface' with set theory, etc.
The workshop will provide a relaxed, constructive atmosphere for an open discussion on both foundational and technical issues. The aim is to obtain an up-to-date picture of the state of the art and to give an impulse to new developments.
Peter Aczel, Thierry Coquand, Per Martin-Löf, Giovanni Sambin, Jan Smith, Silvio Valentini support the initiative and will contribute with a talk.
Any researcher willing to contribute is also invited to participate
and talk; a program committee formed by
Peter Aczel (Manchester - petera@cs.man.ac.uk),
Thierry Coquand (Göteborg - coquand@cs.chalmers.se),
Silvio Valentini (Padova - silvio@math.unipd.it)
will select the relevant contributions based on an abstract due before
September 1 or on direct contact.
Some outstanding exponents of related approaches to topology will also
be invited to join the discussion.
The workshop is organized in the framework of the Working Group Types, with support also from AILA (Associazione Italiana di Logica e Applicazioni) and Dipartimento di Matematica Pura e Applicata, Università di Padova.
The workshop will cover two and a half days, from Thursday morning to Saturday lunch time. It will be held in the historical building of the university, Palazzo del Bo', via 8 Febbraio n.2, in the very center of Padua. No registration fee will be required. No e-mail connections can be provided.
For further information, please contact the organizing committee
Giovanni Sambin - sambin@math.unipd.it,
Giovanni Curi - crigvn44@leonardo.math.unipd.it,
Silvia Gebellato - silvia@math.unipd.it.
The Program Committee - The Organizing Committe