TYPES Summer School 2005

Proofs of Programs and Formalisation of Mathematics

August 15-26 2005

Göteborg, Sweden

[Objective and background, Program and Social Activities, Software Download, Venue, Organisation]

[Accommodation, Grants, Registration and Payment]


Important dates and figures:

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). There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, and other topics with relevant theoretical background. Several talks will be devoted to applications.

During these two weeks we will present three proof assistants: Coq, Isabelle and Agda, three state-of-the-art interactive theorem provers. Participants will get extensive opportunities to use the systems for developing their own proofs.


Program and Social Activities

A tentative list of topics and invited speakers can be found here.

The social activities of the school are described here.

A preliminary schedule can be found here.

Notice that this information might change.


Software Requirements and Instructions

New: Information and "site-specific details" about the software that will be used in the practical sessions with the proof systems (Agda, Coq and Isabelle) can be found here.

It is important that you read this information before arriving to the summer school, so you have the appropriate software installed, and can take part of the practical sessions.



The school will take place at the IT University which is located on Hisingen, to the north of Göta river in the city of Göteborg in Sweden.

The address of the IT University is Forskningsgången 6, Hus Patricia, Lindholmen (map).

More detailed information about the lecture rooms we will use will be provided later.

How to Move Around in Göteborg

You will find answers to most of your questions about public transportation in Göteborg in the Västtrafik pages.

The cheapest way to move around is buying a Maxirabatt 100 card which cost 100 sek. The card is available from many places, in particular kiosks called Pressbyrån (there are a few of those in the bus terminal --called Nils Ericson-- and in the train station, and one at Korsvägen). You can also buy the bus cards in places called Tidpunkten (there is one in the square outside the train station --which is next to the bus terminal-- and one at Brunnsparken). Here you can also ask any information regarding public transportation inside Göteborg.
(Both Brunnsparken and Korsvägen are very well known parts of the town where you might need to change buses and trams.)

To use your card inside a bus or a tram you insert it on the green machines in the vehicle and you press the corresponding button in the machine. When you start your trip you need to press "2" (two coupons equals 13.80 sek and it is the price for an adult during day time within Göteborg). If you are just changing buses to continue the same trip you need to press "byte". A ticket is valid for 90 minutes.

In the back of the card you will be able to see how much money you have left in the card. If the money in the card is not enough to pay the trip the green machine will complain. At this point you can insert a new card or you can pay the difference to the bus driver. In this last case, when changing buses don't put the card in the machine, just show the card and the ticket you got to the driver of the new bus.

You can also pay for a single trip to the bus driver. This will cost you 20 sek.
A daily card cost 50 sek (to be used unlimited inside Göteborg for one day).
Night trips are more expensive, with or without a card.

To see how to get from and to Landvetter airport and from and to the IT University follow the link that corresponds to your accommodation during the school:

Check the page of the Göteborg City airport if you are coming with a Ryanair flight. There you will find information about how to get to the bus terminal.



Students must book their own room. This is done separately from the registration to the school.
We have reserved single and double students rooms in
SGS veckobostäder (student apartments).
Accommodation will cost 4 000 SEK (Swedish crowns) for a single room and 2 400 SEK (per person) for a double room for two weeks. The rooms are paid directly to SGS. Breakfast is not included. There is a shared kitchen one can use.
The booking is done from the web page of SGS . You must use our reservation number 1174 1201 when you book.
If you wish to share a double room with a certain person, please give the complete name of the person you want to share the room with when you book the room. In this case, only one booking is enough for both of you. Be aware that if that person doesn't show up you will have to pay the price for a single room!
If you wish to share a double room but you do not know a person with whom to share the room, simply say so when you register. Please say also if you are male or female.

Questions concerning accomodation at SGS should be put directly to them.



Limited funds are available to offer a few (partial or full) 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 May 20.
Both the recommendation letter and the CV must be sent to school@cs.chalmers.se. 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.

New! When you apply for a grant, please let us know if you are applying for a total grant (travel expenses + room + fee) or for a partial one. If you are applying for a partial grant please specify which of the expenses you want us to cover. In any case, if you would like us to cover the travel expenses please send us an estimation of such cost (in American dollars, euros or Swedish crowns).

Please take into account that even if you get a total grant, there will be small expenses such as public transportation or breakfast (SGS has a kitchen you can share to make your own breakfast at a low price) that you will have to pay yourself.



The registration is now closed. The deadline for registration was June 3. The registration fee is 4 000 SEK (Swedish crowns, 1 euro = 9 SEK) and it has to be paid by June 17. Unpaid registrations will not be considered after this date. The fee includes lunches, dinners, lectures, written material and the excursion.

Any enquires about registration should be sent to school@cs.chalmers.se.


The payment should be made by bank transference to the account below.
To the transference you must add the TYPES Summer School 05 + your complete name. Be aware that if you don't add this information we won't be able to process your payment and hence, your registration will later be discarded.

Organiser information: Chalmers University of Technology
Department of Computer Science and Engineering
412 96 Gothenburg, Sweden
International tax number = VAT no. SE 556479559801
Account information: Nordea Bank Sverige AB
Östra Hamngatan 16
SE-405 09 Göteborg
IBAN-account SE26 3000 0000 0305 57711 371

Please observe that we do not accept payments by credit cards.



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.

Question not concerning accommodation should be sent to school@cs.chalmers.se.

Organising Committee

Andreas Abel, Ana Bove, Thierry Coquand, Peter Dybjer and Bengt Nordström.
Last modified: Mon Aug 29 16:58:16 CEST 2005