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.

Lecturers

Andrea Asperti	Stefano Berardi	Thierry Coquand	Gilles Dowek
Jean-Christophe Filliâtre	Herman Geuvers	Benjamin Gregoire	Tobias Nipkow
Christine Paulin-Mohring	Giovanni Sambin	Andrzej Trybulek	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 Trybulec
13.00-14.30	Lunch	Lunch	Lunch	Lunch	Lunch	Lunch
14.30-16.15	Agda Coquand	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 Gregoire
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.
  
  
• Models
  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.
  
  
• 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.
  
  
• 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.
  
  
• 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.
  
  
• Coq
  
  
• Why
  Christine Paulin-Mohring University of Paris Sud.
  
  
• Krakatoa
  Jean-Christophe Filliâtre University of Paris Sud.
  
  
• Mizar
  
  
• Epigram