From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id DE2C5BC8E for ; Fri, 25 Feb 2005 13:46:53 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j1PCkpBu017540 for ; Fri, 25 Feb 2005 13:46:51 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id NAA07957 for ; Fri, 25 Feb 2005 13:46:51 +0100 (MET) Received: from anubis.medic.chalmers.se (anubis.medic.chalmers.se [129.16.30.218]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j1PCkJYx032434 for ; Fri, 25 Feb 2005 13:46:50 +0100 Received: from [129.16.224.207] (yacc.cs.chalmers.se [129.16.224.207]) by anubis.medic.chalmers.se (Postfix) with ESMTP id 573D0DD63; Fri, 25 Feb 2005 13:46:18 +0100 (CET) Message-ID: <421F1E19.50703@cs.chalmers.se> Date: Fri, 25 Feb 2005 13:46:17 +0100 From: =?ISO-8859-1?Q?Bengt_Nordstr=F6m?= User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.7.3) Gecko/20041006 X-Accept-Language: en-us, en MIME-Version: 1.0 To: types@lists.chalmers.se Cc: appsem@appsem.org, types@cis.upenn.edu, categories@mta.ca, eapls@jiscmail.ac.uk, eacsl@dimi.uniud.it, eatcs-it@cs.unibo.it, acl2@cs.utexas.edu, calculemus-ig@ags.uni-sb.de, caml-list@inria.fr, comlab@comlab.ox.ac.uk, compulog-deduction@cs.bham.ac.uk, coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, lfcs-interest@dcs.ed.ac.uk, members@fmeurope.org, mizar-forum@mizar.uwb.edu.pl, nqthm-users@cs.utexas.edu, nuprllist@cs.cornell.edu, projects-mkm-ig@iu-bremen.de, pvs@csl.sri.com, zforum@prg.ox.ac.uk, www-math@w3.org Subject: Announcement: TYPES Summer School, August 15 - 26 References: <20050217213945.1ae0dccd.hwloidl@informatik.uni-muenchen.de> In-Reply-To: <20050217213945.1ae0dccd.hwloidl@informatik.uni-muenchen.de> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 421F1E3B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; coq:01 miquel:01 tobias:01 nipkow:01 dowek:01 uppsala:01 dybjer:01 coq:01 algebra:01 organising:01 dybjer:01 lambda:01 lambda:01 thierry:01 thierry:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: TYPES Summer School 2005 Proofs of Programs and Formalisation of Mathematics August 15-26 2005, Goteborg, Sweden http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/ During the last ten years major achievements have been made in using computers for interactive proof developments to produce secure software and to show interesting mathematical results. Recent major results are, for instance, the complete formalisation of a proof of the four colour theorem, and a formalisation of the prime number theorem. 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 previous TYPES summer school (in Baastad 1993, Giens 1999, Giens 2002). There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, and other topics with relevant theoretical background. Several talks will be devoted to applications. During these two weeks we will present three proof assistants: Coq, Isabelle and Agda, which are state-of-the-art interactive theorem provers. Participants will get extensive opportunities to use the systems for developing their own proofs. No previous knowledge of type theory and lambda calculus is required. The school is organised by the TYPES working group "Types for Proofs and Programs", which is a project in the IST (Information Society Technologies) program of the European Union. A limited number of grants covering part of travel, fees and ackommodation are available. Neither participation nor grants are restricted to TYPES participants. Lecturers: --------- Jeremy Avigad, Carnegie-Mellon Connor McBride, Nottingham Yves Bertot, INRIA Sophia Alexandre Miquel, Paris 7 Thierry Coquand, Chalmers Tobias Nipkow, TU Munich Catarina Coquand, Chalmers Bengt Nordstrom, Chalmers Gilles Dowek, INRIA Futurs Erik Palmgren, Uppsala Peter Dybjer, Chalmers Christine Paulin, Paris Sud Herman Geuvers, Nijmegen Laurent Thery, INRIA Sophia John Harrison, INTEL Freek Wiedijk, Nijmegen Per Martin-Lof, Stockholm TENTATIVE PROGRAM ----------------- Introduction to Type Theory: Lambda-calculus Propositions-as-types Inductive sets and families of sets Predicative and non-predicative theories Foundations: Introduction to Systems: Coq Isabelle Agda Advanced applications and tools: Proving properties of Java programs Reasoning about Programming Languages Coinduction Correctness of floating-point algorithms Dependently typed programming: Dependently typed datastructures Compiling dependent types Formalisation of mathematics: Introduction Fundamental theorem of algebra Bishop' set theory Other examples, e.g. prime number theorem The organising committee: Andreas Abel, Ana Bove, Catarina Coquand, Thierry Coquand, Peter Dybjer and Bengt Nordstrom.