Program and Social Activities

Proofs of Programs and Formalisation of Mathematics

TYPES Summer School 2005

August 15-26 2005, Göteborg, Sweden

Download

• Lecture Notes distributed during the school: volume 1, volume 2
• Extra material collected during the school (except Connor McBride's Agda and Epigram example files): extra volume

Topics and Invited Speakers

Introduction to Type Theory

• Peter Dybjer: Inductive definitions (slides)
• Herman Geuvers: Lambda-calculus, type systems (notes, exercises, slides 1, slides 2, slides 3, slides 4)
• Alexandre Miquel: Impredicative type theory (slides 1, slides 2, slides 3)
• Bengt Nordström: Types, propositions and problems (notes, slides)

Foundations

• Thierry Coquand: Domain theoretic proofs of normalisation for type theory (slides)
• Gilles Dowek: Mixing deductions and computations (notes, slides)
• Per Martin-Löf: Axiom of Choice

Introduction to Systems

• Yves Bertot, Jean-Christophe Filliatre: Coq (notes, exercices, slides 1, slides 2)
• Catarina Coquand: Agda (slides, list of commands, exercises)
• Tobias Nipkow: Isabelle/HOL (slides, exercises)

Advanced Applications and Tools

• Yves Bertot: Coinduction (notes, slides)
• Jean-Christophe Filliatre: WHY system and Proofs about programs (notes, slides)
• John Harrison: Decision procedures (slides)
• Christine Paulin: Krakatoa Tool for Java Program Verification (slides)
• Laurent Thery: Floating-point algorithms (slides)

Dependently Typed Programming

• Lennart Augustsson: Dependently type programming, some examples (slides)
• Benjamin Gregoire: Compiling dependent types (slides 1, slides 2)
• Connor McBride: Dependently typed datastructures (examples 1 agda, examples 2 agda, examples 3 epigram, Epigram)

Formalisation of Mathematics

• Jeremy Avigad: Formalising the prime number theorem, and foundations for heuristic procedures for the real numbers (notes, slides)
• Herman Geuvers: Fundamental theory of algebra in Coq (slides)
• Erik Palmgren: Bishop' set theory (slides)
• Freek Wiedijk: Formalisation of mathematics (notes 1, notes 2, slides)

[To TYPES School Main Page]

Social Activities

Banquettes and Special Dinner

• The Banquette on Wednesday 17th will take place at Brasserie Ferdinand on Drottninggatan 41 (see map).
• The special dinner on Saturday 20th will take place at Club Avancez on Gibraltargatan 1A (see map).
  The band Biojazz will play for us at the restaurant.
• The Banquette on Wednesday 24th will take place at Skojarbacken on Aschebergsgatan 22 (see map).

Excursion to Marstrand

On Sunday 21st we will have an excursion to the island of Marstrand.

We will go there by boat. The name of the boat is Lasse Dahlquist and it will leave at 9.30 from Lilla Bommen (very near the Opera house, see this map, the dot doesn't really show the place, but it is written "Lilla Bommenshamns").

We will arrive at Marstrand around 12.00.
We have booked the lunch at 12.30 in Villa Maritime at 12.30. When coming out of the boat, we should turn to the left.

After the lunch there are no other activities planned as a group so each person can stay in the island as long as he/she wants. There are very nice bathing places so do not forget to bring your sun protection and your swimming clothes!

To return to Gothenburg one can take regular public buses. The buses (312 and 302) go about once an hour until 18.30. Possible there is 1 or 2 more buses after that time. Please check the schedule on time.
The trip cost 50 sek if you pay to the driver or 5 coupons with the Maxirabatt card. the trip to Nils Ericson terminal takes about 60 minutes.