The Coq mailing list

[Bengt Nordstr�m <bengt AT cs.chalmers.se>]

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.