Logic List Mailing Archive

(no subject)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



                    SECOND WORKSHOP ON FORMAL TOPOLOGY

               Auditorium S. Margherita, Campo S. Margherita
                         Venice, April 4-6, 2002

organised by:
the EC Types Working Group
Dipartimento di Matematica Pura e Applicata, Universita' di Padova
Dipartimento di Informatica, Universita' Ca' Foscari, Venezia

This workshop is about a specific approach to formal, or
pointfree, topology, which stresses its constructive features.
Its historical roots include Brouwer's conception of the
continuum, which was expressed in terms of choice sequences.  
The later analysis and elimination of choice sequences led to
connections with locale theory and inductive definitions, as in
Martin-Loef's Notes on constructive mathematics.  So it aims at
a theory of formal spaces, in some way similar to the present
impredicative theory of locales, but expressed in a predicative
constructive framework such as constructive type theory
(Martin-Loef)  or constructive set theory (Aczel).


As time passed, the landscape of formal topology has become
wider, and its distinctive predicative foundation has given rise
to some unexpected mathematical developments (even the right
approach to the notion of a `closed set' needs a conceptually
new approach, where `closed' is not the complement of `open').  
Nowadays it includes a variety of themes and novelties, which
are of interest in:

- computer science, because of the methods of definition by
induction and recently also by co-induction, the techniques for
the extraction of constructive information from a priori non
effective arguments and connections with domain theory,
implementation problems, etc.;

- logic and foundations, because of the interaction between the
foundations of mathematics and the actual development of
mathematics, methods from proof theory in the practice of
mathematics, sheaf models, the logical nature of topological
definitions, etc.;

- mathematics itself, because of the process of
constructivization - which often is accompanied by a conceptual
simplification - of classical results of topology and of
mathematics in general and also the connections with category
theory and locale theory, etc..

The first workshop of this series took place in Padova, October
1997. It was widely appreciated for its relaxed and constructive
atmosphere, and for an open discussion on various approaches.  
Hopefully with a similar atmosphere, the aim of the second
workshop will be to obtain an up-to-date picture of the
foundational and technical issues concerning formal topology,
and to clarify the connections with related approaches.

Invited speakers. The list of invited speakers at the moment
includes Martin Escardo, Henri Lombardi, Peter Johnstone, Erik
Palmgren, Mike Smyth, Steve Vickers.

Tutorials.  The workshop will be preceeded by one day, 3 April
2002, of tutorials to help those people who are interested but
have little or even no knowledge of formal topology.  At the
moment, Peter Aczel and Giovanni Sambin have volunteered.

Contributed papers. Those who wish to contribute with a half
hour talk, should submit a summary of contents (from 1 to 10
pages) to Thierry Coquand, coquand@cs.chalmers.se by 28 February
2002. The program committe will notify acceptance by 15 March
2002.

Proceedings. The proceedings will be published after the
workshop, probably, a special issue of some good journal (hence
with referees and open also to nonparticipants)

Registration. Registration is free; the form below must be sent
to Giovanni Curi, gcuri@math.unipd.it. A convenient accomodation
in Venice can be provided only to those participants who
register by 30 September 2001. For a low cost accomodation
(possibily in a common room), contact Claudia Faggian
claudia@math.unipd.it

Grants. We also plan to offer a limited number of grants for
students and young researchers covering accomodation and food.
Please send a short CV and motivations for participation to
Giovanni Sambin sambin@math.unipd.it

Site. Venice needs no presentation. But note that the site of
the workshop is out of the main tourist routes, and should allow
for an appreciation of the popular and historical aspects of the
city. We expect to find convenient accomodations nearby.

Social Program. A trip will be organized for those who remain on
Sunday 7 April 2002. An idea is to hire a boat and have lunch in
an island of the lagoon. The full social program will be
communicated later.

Second announcment. The second announcement will contain
information updates and the web address of a page dedicated to
the workshop (with details on place, accomodation, tourist
information, trip, etc.).

The program committee

Peter Aczel
Thierry Coquand
Per Martin-Loef (chair)
Giovanni Sambin (local organization)
Dieter Spreen



dates:

September 30, 2001 : early registration (with safe accomodation)

February 28, 2002: deadline for the submission of papers

March 15, 2002: program is decided

April 3, 2002: tutorials

April 4 - 6, 2002:  workshop

April 7: trip for those who wish to remain, probably on a
privately hired boat


Registration Form:

Name and Family name:
Institution:
Address:
E-mail address:
Date of arrival:                  Date of departure:
Kind of accomodation (if required):
low cost (common room, around 8 beds, price around 15 euros)
single room (Fondazione Levi or Palazzo Zenobio, price around 50
euros, maybe less)
double-triple room (Fondazione Levi or Palazzo Zenobio, price
around 35 euros)