[TYPES/announce] Types Summer School 07: Deadline for grants approaching

[Claudio Sacerdoti Coen]

                    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 at 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 at cs.unibo.it

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: sacerdot at cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------