Esprit working group 21900: Types for Proofs and Programs

Types Summer School'99:

Theory and Practice of Formal Proofs

Giens, France
August 30 - September 10, 1999


Objective and background

During the last few years major achievements have been made in using computers for interactive proof developments to produce secure software.
This two weeks' course is for postgraduate students, researchers and industrials who want to learn about interactive proof development. There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, and other topics which give relevant theoretical background. Several talks will be devoted to the presentation of applications.
The proof assistants presented in the school represent the current state-of-the-art in interactive theorem proving. Participants will get extensive opportunities to use the systems in a workstation environment for developing their own proofs.

Location and accommodation: See the venue information.

The summer school takes place in a holiday village in the peninsula of Giens, facing the well known most beautiful islands in the French Riviera: Porquerolles and Port-Cros (boats to there every hour, every day). It is located in 34 hectars of pine forests, with a few tranquil inlets to explore. There will be many (sea-side or not) activities available, including scuba diving, catamarans, windsurfer rental, sea canoe hire, montain bike, jogging, tennis, etc.

Program

Lecture Notes

Social event:

An excursion will be organized to the Porquerolles Island on Sunday September 5th.

Systems: To download the systems to be used in the course.

List of participants

Some pictures


Logistics:

Application

Send your application form to Joëlle Despeyroux. Note that a (short) letter of recommendation should be sent in addition to the application form; This letter is only needed for students, or people not having a PhD degree.
The deadline for application is Monday May 17, 1999. All applicants will receive notice by Friday May 21, 1999. A registration form will then have to be sent (see the "Registration" paragraph below).

Registration

People having been accepted as participants to the school, as well as lecturers and free participants (*) are kindly asked to fill the electronic registration form. The deadline for registration is Monday June 14, 1999. This dead-line is firm.
Feel free to contact Monique Simonetti for any further informations.

(*) Definition. A free participant is not willing to attend the all event, but only part of it. He typically plans to come only for a few days, following some of the talks, eventually none. In any case he is not interested in working in the lab.

Registration fees

The registration fees, including all expenses (lecture material, accomodation, all meals, coffee break refreshments and social events, during the 12 days) are 6,200 FF per participant.

Grant

Limited funds will be available to offer a few grants. In particular, participants from lower-income countries might get a grant covering a substantial part of the costs for travel and subsistence.
The dead-line for application for a grant is Friday April 2. You will receive notification of acceptance/rejection by Monday April 19.
To apply for a grant, fill the required parts of the application for a grant form.

Organizing / Program Committee

  • Joelle.Despeyroux, INRIA (Chair)
  • Gilles Dowek, INRIA
  • Martin Hofmann, University of Edinburgh
  • Bengt Nordstrom, Chalmers University
  • Organisation

    Joëlle Despeyroux and Monique Simonetti
    Address: INRIA, 2004, route des Lucioles B.P.93, 06902 Sophia-Antipolis Cedex, France.
    Email: Joelle.Despeyroux@inria.fr, Monique.Simonetti@inria.fr
    Phone: +33 04 92 38 78 05, __78 64 -- Fax: +33 04 92 38 76 33, __79 55
    Sponsors:
    Joelle.Despeyroux@inria.fr