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 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.
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
Monday Tuesday Wednesday Thursday Friday Saturday 09.00-10.45 Introduction
13.00-14.30 Lunch Lunch Lunch Lunch Lunch Lunch 14.30-16.15 Agda
Excursion Isabelle-lab Isar-lab Mizar-lab 16.45-18.30 Agda-lab Agda-lab Excursion Isabelle-lab Isar-lab Mizar-lab
Monday Tuesday Wednesday Thursday Friday Saturday 09.00-10.45 Inductive Constructions
Coq-lab Proof Carrying Code
Proof Carrying Code
Coq Coq-lab Why
Epigram 13.00-14.30 Lunch Lunch Lunch Lunch Lunch 14.30-16.15 Matita-lab Coq-lab Free Krakatoa
Epigram-lab 16.45-18.30 Matita-lab Coq-lab Free Why-Krakatoa
- Introduction to type theory
Herman Geuvers, Radboud University Nijmegen.
Slides-1 Slides-2 Slides-3 Slides-4
Thierry Coquand, Goeteborg University.
- 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.
- Proof Carrying Code
Benjamin Gregoire, INRIA, Sophia Antipolis.
Slides 2 Slides 3 Other Material
David Pichardie, INRIA, Rennes
Overview Slides 1 Slides 4
Ulf Norell, Chalmers University
Agda is a dependently typed programming language with good support for programming with inductively defined families of types.
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.
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.
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
Jean-Christophe Filliâtre University of Paris Sud.
Notes Slides Lab
Jean-Christophe Filliâtre University of Paris Sud.
Course on Mizar by Adam Naumowicz
Thorsten Altenkirch, University of Nottingham
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 email@example.com. 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.
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 firstname.lastname@example.org
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi.