[Prev][Next][Index][Thread]

announcement of a congress


Dear Colleague,

A meeting on type theory will take place on October 19-21
this year in Venice. The main subject of the meeting is
the intuitionistic type theory that Per Martin-Lof
started developing in 1970. This is reflected in the
festive title of the meeting

     "Twenty-Five Years of Constructive Type Theory",

but we also want some related developments to be taken
into account at the meeting. The program will display the
various points of view from which type theory has been
approached, including logic and foundations of mathematics,
computing science, philosophy and linguistics.

There will be two and a half days of talks, followed by
a round table discussion on the background and possible
future lines of development of type theory.
A list of speakers and discussants is appended to
this letter.

 A limited number of places is still available for
registration, and a still smaller number for accomodation
in Venice at a reasonable price. More detailed information
on this and on other practical arrangements will be sent
on request

  Giovanni Sambin       Jan von Plato

  (on behalf of the program committee)

                          *   *   *

            Twenty-Five Years of Constructive Type theory

           October 19-21, 1995, by Ateneo Veneto, Venice

Place: Ateneo Veneto, Campo S. Fantin 1897, 30124 Venezia (Italy)

Program committee: Giovanni Sambin, chair (University of Padua), Furio
Honsell (University of Udine), Jan Smith (Chalmers University), Goran
Sundholm (University of Leiden), Jan von Plato (University of Helsinki)

Invited speakers:
 Peter Aczel: title to be announced
 Stefano Berardi: An isomorphism between classical and intuitionistic proofs
 Rod Burstall: title to be announced
 Thierry Coquand: Formal Topology and Constructive Type Theory
 Martin Hofmann: Groupoid interpretations of Martin-Loef's type theory and
        applications thereof
 Petri Maenpaa: Parsing in type theory
 Lena Magnusson: Interactive proof construction in type theory
 Per Martin-Loef: title to be announced
 Christine Paulin: Proofs and Programs in the Calculus of Inductive
         Constructions
 Aarne Ranta: Grammatical rules for proof texts
 Anton Setzer: Proof Theory and Martin-Loef Type Theory
 Goeran Sundholm: Inference, consequence, implication
 William Tait: title to be announced
 Silvio Valentini: Building up a toolbox for Martin-Loef's Type Theory,
 Dirk van Dalen: title to be announced

Round table:
  N. G. de Bruijn, Robert L. Constable (Experience with Constructive Type
 Theory as a Foundation for Computer Science), Jean-Yves Girard,

Arrival date is Wednesday, October 18th. Departure day is Sunday the 22nd.
Talks will begin on Thursday morning.  We plan to organize a boat trip or
similar on Sunday, for participants who wish to delay their departure by
one day.
No inscription or accomodation forms are required.
Contact (preferably by e-mail) to:

  Giovanni Sambin at sambin@pdmat1.math.unipd.it
  Dipartimento di Matematica Pura e Applicata, Universita' di Padova
  Via Belzoni 7
  35131 Padova (Italy)

  or

  Jan von Plato at vonplato@cc.helsinki.fi
  University of Helsinki
  Department of Philosophy
  P.O. Box 24
  SF-00014 University of Helsinki
  (Finland)