Mathematical Logic in Padua

home | events | 2WFTop

Events

Second Workshop on Formal Topology (2WFTop 2002)

Venice April 4-6, 2002
organized by
the EC TYPES Working Group
Dipartimento di Matematica Pura ed Applicata, Università di Padova
Dipartimento di Informatica, Università di 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-Löf'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, b ut expressed in a predicative constructive framework such as constructive type theory (Martin-Löf) 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

Bernhard Banaschewski (McMaster University, Canada)
Martin Escardò (University of Birmingham, United Kingdom)
Peter Johnstone (University of Cambridge, United Kingdom)
Henri Lombardi (CNRS, Universite de Franche-Comte)
Chris Mulvey (University of Sussex, United Kingdom)
Erik Palmgren (University of Uppsala, Sweden)
Mike Smyth (Imperial College, United Kingdom)
Steve Vickers (Open University, United Kingdom)

Tutorials: 3 April 2002

Bernhard Banaschewski (McMaster University, Canada)
Peter Aczel (University of Manchester, United Kingdom)
Giovanni Sambin (University of Padova, Italy)
Silvio Valentini (University of Padova, Italy)

Program

The workshop begins on Thursday 4 April 2002, at 9.00 with opening by Per Martin-Löf, and ends on Saturday 6 April 2002, around 17.00. Draft program

Program Committee

Peter Aczel (University of Manchester, United Kingdom)
Thierry Coquand (University of Chalmers, Sweden)
Per Martin-Löf (chair, University of Stockholm, Sweden)
Giovanni Sambin (organizer, University of Padova, Italy)
Dieter Spreen (University of Siegen, Germany)

Proceedings

The proceedings will be published after the workshop, as a special issue of Annals of Pure and Applied Logic and will be open also to non-participants.

Registration

Registration is free. Please send name, addresses, date of arrival and departure, to Damiano Macedonio. For accomodation, one can now address directly to Palazzo Zenobio, were many of the participants will lodge. Travel, accomodation and social program