TYPES Summer School'02:
Theory and Practice of Formal Proofs
Giens, France, September 2-13, 2002
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.
The present school follows the format of the previous
Types summer school:
Types'99.
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 informations.
The summer school will take 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). The village 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.
Systems:
To download the systems presented in the course.
The previous Types summer school:
Types'99.
Registration to the school is in 2 stages:
1) Application
Participation to the school is subject to acceptation by the
program committee.
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 not having a PhD degree.
The deadline for application is Friday april 19, 2002;
In the case you apply for a grant,
send your application form a week before: Friday April 12, 2002
(see below).
All applicants will receive notification of acceptance/rejection
by Monday May 13, 2002.
2) Registration
People having been accepted as participants to the school
(see the above "Application" paragraph), as well as
lecturers and free participants, are kindly asked to fill the
electronic registration form
before Friday May 31, 2002.
Please ask Monique Simonetti for any further questions.
Registration fees
The registration fees, including all expenses (lecture material,
accomodation, all meals, coffee break, refreshments and tour on the
Porquerolles island, during the 12 days) are 1000 Euros per
participant.
Grants
Limited funds will be available to offer a few (partial or full) grants.
The deadline for application for a grant is Friday April 12, 2002.
You will receive notification of acceptance/rejection by
Tuesday April 30, 2002.
To apply for a grant, fill the required parts of the
application form.
Feel free to contact
Monique Simonetti for any further informations.
Program Committee:
Stefano Berardi, Joelle Despeyroux (chair), Peter Dybjer,
Herman Geuvers, Zhaohui Luo, Martin Hofmann, Benjamin Werner.
Organizing Committee:
Yves Bertot, Joelle.Despeyroux, Francis Montagnac,
Monique Simonetti, Benjamin Werner.
Organisation
Contact:
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:
Vinci
Joëlle Despeyroux,
Joelle.Despeyroux@inria.fr.
IST European project 29001:
Computer-Assisted Reasoning based on Type Theory (TYPES)