August 19-31th, 2007

BERTINORO - ITALY

( Residential Centre of the University of Bologna)

A preliminary **live CD** image is available for download at the
ITPLive homepage.
The software is almost in shape, but more documentation and exercises
will be added later, so we suggest to burn the image on a rewritable media.

**Laptops and software for the summer school:** participants are supposed
to bring their own laptop. Before the start of the school, we will send you a
live-CD image for a Linux distribution (debian based) with all proof assistants
already installed.

**Accomodation:** accomodation in the Bertinoro Residential Center will
be provided to everybody until the 1st September morning. We plan to have
shuttles to Forli's train station the 1st Semptmber morning, but we will
schedule them during the school, according to the participants needs.

**Shuttles:** on Sunday 19th there will be regular buses connecting
Forli's train station with Bertinoro at 15:10 and 19:10. We also plan to have
shuttles from Forli's trains station at about 16:30, 18:30 and 19:30.

**Reception time:** participants will be lodged in the Residential Center
that does not have a permanent reception. The reception will be opened between
18:00 and 21:00. Those arriving before 18:00 can leave the luggage at the
residential center and enjoy Bertinoro.

More information will be provided by the Residential Center a few days before the conferences. Additional informations may happear on this page.

During the last ten years major achievements have been made in using computers forinteractive proof developmentsto producesecure softwareand 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.This two weeks' course is 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 Båstad 1993, Giens 1999, Giens 2002 and Goeteborg 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.

- 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).

Registration must be made on line at this site.

Thorsten AltenkirchAndrea AspertiStefano BerardiThierry CoquandJean-Christophe FilliâtreHerman GeuversBenjamin GregoireTobias NipkowChristine Paulin-MohringUlf NorellDavid PichardieGiovanni SambinAndrzej TrybulecMarkus Wenzel

First weekMonday Tuesday Wednesday Thursday Friday Saturday 09.00-10.45 Introduction

GeuversIntroduction

GeuversProgram extraction

BerardiFormal Topology

SambinModels

CoquandFormal Topology

Sambin11.15-13.00 Introduction

GeuversIntroduction

GeuversModels

CoquandIsabelle

NipkowIsar

WenzelMizar

Naumowicz13.00-14.30 Lunch Lunch Lunch Lunch Lunch Lunch 14.30-16.15 Agda

NorellProgram extraction

BerardiExcursion Isabelle-lab Isar-lab Mizar-lab 16.45-18.30 Agda-lab Agda-lab Excursion Isabelle-lab Isar-lab Mizar-lab Second weekMonday Tuesday Wednesday Thursday Friday Saturday 09.00-10.45 Inductive Constructions

PaulinInductive Constructions

PaulinCoq-lab Proof Carrying Code

GregoireProof Carrying Code

Pichardie11.15-13.00 Matita

AspertiCoq Coq-lab Why

FilliâtreEpigram 13.00-14.30 Lunch Lunch Lunch Lunch Lunch 14.30-16.15 Matita-lab Coq-lab Free Krakatoa

PaulinEpigram-lab 16.45-18.30 Matita-lab Coq-lab Free Why-Krakatoa

-labEpigram-lab

Introduction to type theory

Herman Geuvers, Radboud University Nijmegen.

Slides-1 Slides-2 Slides-3 Slides-4

Models

Thierry Coquand, Goeteborg University.

Slides-1 Slides-2

Realizability: Extracting Programs from proofs

Stefano Berardi, Universita' di Torino.

In this 4-hours course we sketch the Realizability Interpretation, then an optimization method for realizers, called Dead Code Analysis. Realizability interpretation takes a constructive proof of the existence on an object with a given property, and turns it into a program finding such an object. The programs we find in this way are simple-minded, but they effectively depends on the ideas of the proof. Dead-code analysis turns these simple-minded program into more efficient ones.

Slides

Proof Carrying Code

Benjamin Gregoire, INRIA, Sophia Antipolis.

Slides 2 Slides 3 Other Material

David Pichardie, INRIA, Rennes

Overview Slides 1 Slides 4

Agda

Ulf Norell, Chalmers University

Agda is a dependently typed programming language with good support for programming with inductively defined families of types.

Exercises

Isabelle

Tobias Nipkow, Technischen Universität München.

We introduce Isabelle/HOL by showing how to write and verify functional programs. Proofs will follow the induction + simplification style, using the traditional tactical approach. Heuristics for generalizing inductive goals are explained.

Slides-and-Exercises

Isar

Markus Wenzel, Technischen Universität München.

The Isar proof language allows structured proof composition in the Isabelle framework, such that the resulting proof text is both human-readable and checkable by the machine (optionally with explicit proof terms). We give an introduction to the main techniques for practical Isar proof composition, together with some theoretical foundations as required. This will essentially teach the ``first letters'' in the Isar language, to get started with further practice of reading and writing of Isar proofs.

Isar-quickref Exercises

Matita

Andrea Asperti, Universita' di Bologna.

Matita (that meanspencilin italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna. Matita is based on the Calculus of (Co)Inductive Constructions, and is compatible, at some extent, with Coq. It is a reasonably small and simple application, whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions. Matita has both a procedural and a declarative editing mode; (XML-encoded) proof objects are produced for storage and exchange.

Exercises (includes a short tutorial)

Matita Tutorial by Andrea Asperti (under construction)

A page in number theory by Andrea Asperti

Inductive Constructions

Slides

Coq

Why

Jean-Christophe Filliâtre University of Paris Sud.

Notes Slides Lab

Krakatoa

Jean-Christophe Filliâtre University of Paris Sud.

Mizar

Course on Mizar by Adam Naumowicz

Slides Exercises

Epigram

Thorsten Altenkirch, University of Nottingham

Material

## 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.

## Organisation

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.

Any question concerning the school may be sent to typessummerschool@cs.unibo.it

## Organising Committee

Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi.