Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Tue, 26 Jan 1993 15:29:01 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03358; Tue, 26 Jan 93 07:17:49 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from animal.cs.chalmers.se by ted.cs.uidaho.edu (16.6/1.34) id AA03351; Tue, 26 Jan 93 07:17:41 -0800 Date: Tue, 26 Jan 93 16:17:14 +0100 From: Peter Dybjer Message-Id: <9301261517.AA00179@animal.cs.chalmers.se> Received: from muppet93.cs.chalmers.se by animal.cs.chalmers.se (5.60+IDA/3.14+gl) id AA00179; Tue, 26 Jan 93 16:17:14 +0100 Received: by muppet93.cs.chalmers.se (5.60+IDA/3.14+gl) id AA00635; Tue, 26 Jan 93 16:17:13 +0100 To: info-hol@edu.uidaho.cs.ted Subject: summer school Could you please send the following announcement to the HOL-mailing list? Peter Dybjer ------------------------------------------------------------------------------ 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.