List of participants


Final version of the Live CD with all slides/exercices/...

Latest news!!!

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.

Objective and background

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.

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.

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).
  
  Registration must be made on line at this site.

Lecturers

Thorsten Altenkirch	Andrea Asperti	Stefano Berardi	Thierry Coquand
Jean-Christophe Filliâtre	Herman Geuvers	Benjamin Gregoire	Tobias Nipkow
Christine Paulin-Mohring	Ulf Norell	David Pichardie	Giovanni Sambin
Andrzej Trybulec	Markus Wenzel

Program

First week
	Monday	Tuesday	Wednesday	Thursday	Friday	Saturday
09.00-10.45	Introduction Geuvers	Introduction Geuvers	Program extraction Berardi	Formal Topology Sambin	Models Coquand	Formal Topology Sambin
11.15-13.00	Introduction Geuvers	Introduction Geuvers	Models Coquand	Isabelle Nipkow	Isar Wenzel	Mizar Naumowicz
13.00-14.30	Lunch	Lunch	Lunch	Lunch	Lunch	Lunch
14.30-16.15	Agda Norell	Program extraction Berardi	Excursion	Isabelle-lab	Isar-lab	Mizar-lab
16.45-18.30	Agda-lab	Agda-lab	Excursion	Isabelle-lab	Isar-lab	Mizar-lab
Second week
	Monday	Tuesday	Wednesday	Thursday	Friday	Saturday
09.00-10.45	Inductive Constructions Paulin	Inductive Constructions Paulin	Coq-lab	Proof Carrying Code Gregoire	Proof Carrying Code Pichardie
11.15-13.00	Matita Asperti	Coq	Coq-lab	Why Filliâtre	Epigram
13.00-14.30	Lunch	Lunch	Lunch	Lunch	Lunch
14.30-16.15	Matita-lab	Coq-lab	Free	Krakatoa Paulin	Epigram-lab
16.45-18.30	Matita-lab	Coq-lab	Free	Why-Krakatoa -lab	Epigram-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 means pencil in 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.