Summer School on Type Theory
INTERNATIONAL SUMMER SCHOOL
TYPES FOR PROOFS AND PROGRAMS
BAASTAD, SWEDEN, JUNE 7 - 18, 1993
During the last few years major achievements have been made in using
computers for interactive proof developments. Several proof assistants
(such as Coq, Lego, and Alf) have been developed based on the idea of
a logical framework in which it is possible to define a variety of
logics. Many quite substantial proofs from mathematics, logic, and
computing have also been implemented in them.
This two week course is for postgraduate students and researchers 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 background. No prior knowledge of these topics is expected.
The systems will be demonstrated, and students will get extensive
opportunities to use them in a workstation environment for developing
their own proofs.
List of speakers
The main speakers are
Henk Barendregt Jean-Louis Krivine
Stefano Berardi Per Martin-Lof
Rod Burstall Michel Parigot
Thierry Coquand Christine Paulin
Gerard Huet Randy Pollack
The summer school will be held in Baastad, a small town between
Copenhagen and Gothenburg on the Swedish west coast.
There is a limited number of scholarships available for people who
cannot obtain funding for their travel, participation fee and living
expenses. A request for full or partial support should be enclosed
with the application.
The participation fee is 4 000 SEK and room and board is 4 000 SEK.
Applications with a C.V. and a letter of recommendation should be sent
- summer school -
Department of Computer Sciences
Chalmers Technical University
S - 412 96 Gothenburg, Sweden
The DEADLINE for application is April 15, 1993.
The school is organized by the ESPRIT Basic Research Action `Types for
Proofs and Programs'. The local organization is done by Bengt
Nordstrom, Peter Dybjer, Jan Smith, and Bjorn von Sydow, Gothenburg.