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

Summer School on Type Theory




			 INTERNATIONAL SUMMER SCHOOL
				      ON
			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

Location
--------
The summer school will be held in Baastad, a small town between
Copenhagen and Gothenburg on the Swedish west coast.

Scholarships
------------
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.

Fees
----
The participation fee is 4 000 SEK and room and board is 4 000 SEK.

Applications
------------
Applications with a C.V. and a letter of recommendation should be sent
to
        Bengt Nordstrom
        - summer school -
        Department of Computer Sciences
        Chalmers Technical University
        S - 412 96 Gothenburg, Sweden
        e-mail:baastad@cs.chalmers.se

The DEADLINE for application is April 15, 1993.

Organization
------------
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.