From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 9EFABBC8E for ; Wed, 4 May 2005 10:37:32 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j448bTr3009721 for ; Wed, 4 May 2005 10:37:29 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA14589 for ; Wed, 4 May 2005 10:37:29 +0200 (MET DST) Received: from anubis.medic.chalmers.se (anubis.medic.chalmers.se [129.16.30.218]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j448bSsW023551 for ; Wed, 4 May 2005 10:37:29 +0200 Received: from [129.16.224.207] (yacc.cs.chalmers.se [129.16.224.207]) by anubis.medic.chalmers.se (Postfix) with ESMTP id 41EDC3FBB; Wed, 4 May 2005 10:37:27 +0200 (CEST) Message-ID: <427889C0.50104@cs.chalmers.se> Date: Wed, 04 May 2005 10:37:20 +0200 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: mizar-forum@mizar.uwb.edu.pl, projects-mkm-ig@iu-bremen.de, eapls@jiscmail.ac.uk, calculemus-ig@ags.uni-sb.de, lfcs-interest@dcs.ed.ac.uk, categories@mta.ca, comlab@comlab.ox.ac.uk, appsem@appsem.org, acl2@cs.utexas.edu, zforum@prg.ox.ac.uk, pvs@csl.sri.com, caml-list@inria.fr, eacsl@dimi.uniud.it, isabelle-users@cl.cam.ac.uk, members@fmeurope.org, types@cis.upenn.edu, eatcs-it@cs.unibo.it, nqthm-users@cs.utexas.edu, coq-club@pauillac.inria.fr, www-math@w3.org, nuprllist@cs.cornell.edu, compulog-deduction@cs.bham.ac.uk Subject: Announcement: TYPES Summer School, August 15 - 26 References: <20050217213945.1ae0dccd.hwloidl@informatik.uni-muenchen.de> <421F1E19.50703@cs.chalmers.se> In-Reply-To: <421F1E19.50703@cs.chalmers.se> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 427889C9.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 427889C8.001 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 2005,:98 lambda:01 lambda: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: Important deadlines: May 20: Grant application, June 3: registration It is now possible to register for the course! 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. See the following articles in The Economist and Science: http://www.economist.com/science/displayStory.cfm?story_id=3809661 http://www.sciencemag.org/cgi/content/full/307/5714/1402a The summer school is a two weeks' course 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.