Logic List Mailing Archive

Second Workshop on Formal Topology, Venice, April 2002 (fwd)

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)