From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.9 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 04276BC0A for ; Wed, 23 May 2007 11:35:05 +0200 (CEST) Received: from leb.cs.unibo.it (leb.cs.unibo.it [130.136.1.102]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l4N9Z4Rq018443 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Wed, 23 May 2007 11:35:04 +0200 Received: from faust.cs.unibo.it (faust.cs.unibo.it [130.136.5.135]) by leb.cs.unibo.it (Postfix) with ESMTP id A044117FDF; Wed, 23 May 2007 11:34:01 +0200 (CEST) Received: by faust.cs.unibo.it (Postfix, from userid 2662) id 13EC237C81; Wed, 23 May 2007 11:35:02 +0200 (CEST) Date: Wed, 23 May 2007 11:35:02 +0200 From: Claudio Sacerdoti Coen To: mizar-forum@mizar.uwb.edu.pl, projects-mkm-ig@iu-bremen.de, grin@di.unipi.it, mowgli-dev@cs.unibo.it, calculemus-ig@ags.uni-sb.de, coq-club@pauillac.inria.fr, caml-list@yquem.inria.fr, types-wg@durham.ac.uk, types-announce@lists.seas.upenn.edu, map@fourier.ujf-grenoble.fr, types@lists.chalmers.se Subject: Types Summer School 07: Deadline for grants approaching Message-ID: <20070523093502.GT6946@cs.unibo.it> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit X-Operating-System: Debian GNU/Linux X-Organization: Department of computer science, University of Bologna, European Union User-Agent: Mutt/1.5.11 X-Miltered: at concorde with ID 46540AC8.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; sacerdoti:01 coen:01 sacerdot:01 unibo:01 unibo:01 lambda:01 topology:01 coq:01 thorsten:01 torino:01 coquand:01 filliatre:01 gregoire:01 tobias:01 nipkow:01 TYPES Summer School 2007 Proofs of Programs and Formalisation of Mathematics August 19-31 2007, Bertinoro, Italy http://TypesSummerSchool07.cs.unibo.it >>>>>>> DEADLINE FOR GRANTS: JUNE 4th <<<<<<<< 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. 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 and Goteborg 2005). There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, proof carrying code, formal topology and models, with relevant theoretical background. Several talks will be devoted to applications. During the two weeks, participants will get extensive opportunities to use and compare most ot the current tools for the automation of formal reasoning, comprising Agda, Coq, Epigram, Matita, Mizar and Isabelle/ Isar. 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. Grants covering part of travel, fees and accommodation are available. Neither participation nor grants are restricted to TYPES participants. Grants ------ To apply for a grant you are required to send a recommendation letter and a CV or a similar short description of yourself. All information/documentation concerning grant applications must reach us by June 4. Both the recommendation letter and the CV should be sent to typessummerschool@cs.unibo.it. Please use the subject: "grant application". The recommendation letter must be sent to us directly by the person that writes it. We will confirm by email each CV and recommendation letter we receive. Important dates and figures --------------------------- * June 4: deadline for grant applications. * June 25: deadline for inscription With double room accomodation: 1100 Euros. With single room accomodation: 1300 Euros. The fee is all inclusive (accomodation, meals, school participation fees, and social activities). Confirmed Lecturers ------------------- Thorsten Altenkirch, Nottingham Andrea Asperti, Bologna Stefano Berardi, Torino Thierry Coquand, Chalmers Jean-Christophe Filliātre, Paris Sud Herman Geuvers, Nijmegen Benjamin Gregoire, INRIA Sophia Tobias Nipkow, TU Munich Christine Paulin-Mohring, Paris Sud David Pichardie, IRISA Rennes Giovanni Sambin, Padova Andrzej Trybulec, Bialystok Markus Wenzel, TU Munich TENTATIVE PROGRAM ----------------- Introduction to Type Theory: Lambda-calculus Propositions-as-types Inductive sets and families of sets Predicative and non-predicative theories Model Theory Introduction to Systems: Agda Coq Epigram Isabelle/Isar Mizar Matita Why/Krakatoa Advanced topics: Program extraction Proving properties of Java programs Reasoning about Programming Languages Proof Carrying Code Dependently typed programming languages Formal Topology ORGANIZING COMMITTEE -------------------- Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi Any question concerning the school may be sent to typessummerschool@cs.unibo.it -- ---------------------------------------------------------------- Real name: Claudio Sacerdoti Coen Doctor in Computer Science, University of Bologna E-mail: sacerdot@cs.unibo.it http://www.cs.unibo.it/~sacerdot ----------------------------------------------------------------