Announcement: TYPES Summer School, August 15  26

Bengt_Nordström
 Bengt_Nordström
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Bengt_Nordström <bengt@c...> 
Subject:  Announcement: TYPES Summer School, August 15  26 
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 1526 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 stateoftheart 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, CarnegieMellon 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 MartinLof, Stockholm TENTATIVE PROGRAM  Introduction to Type Theory: Lambdacalculus Propositionsastypes Inductive sets and families of sets Predicative and nonpredicative theories Foundations: Introduction to Systems: Coq Isabelle Agda Advanced applications and tools: Proving properties of Java programs Reasoning about Programming Languages Coinduction Correctness of floatingpoint 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.