TYPES Summer School 2007

TYPES Summer School 2007
Proofs of Programs and Formalisation of Mathematics

August 19-31 2007, Bertinoro, Italy

http://TypesSummerSchool07.cs.unibo.it

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 of 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. A limited number of grants covering part of travel, fees and ackommodation are available. Neither participation nor grants are restricted to TYPES participants.

Grants

A large amount of money is available to offer travel grants. To apply for a grant you must provide a recommendation letter and a CV or a similar short description of yourself. All information/documentation concerning a grant applications must reach us by June 4.

Both the recommendation letter and the CV must 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 (travel only).
  • 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

Andrea Asperti, Bologna
Stefano Berardi, Torino
Thierry Coquand, Chalmers
Jean-Christophe Fillitre, Paris Sud
Herman Geuvers, Nijmegen
Benjamin Gregoire, INRIA Sophia
Tobias Nipkow, TU Munich
Christine Paulin-Mohring, Paris Sud
Giovanni Sambin, Padova
Andrzej Trybulek, 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

Leave a Reply

Your email address will not be published. Required fields are marked *