Software requirements and instructions

TYPES Summer School 2005

August 15-26 2005, Göteborg, Sweden

Software to install and use in the practical sessions

There will be exercises in Agda, Coq and Isabelle. Participants who borrow a laptop from the summer school will have the above systems pre-installed,
and those who bring their own laptops should install the necessay software themselves, before Aug 15. On this page we provide some information to help with the installation of the necessary software.

There will be wireless network access for the registered participants, and for people with chalmers accounts (cid). If you bring your own laptop, make sure you have a working wireless connection in your computer. We will also provide a CD and USB memory with the base software, in case of network problems.



The version used will be Coq-8.0pl2. The binary installation will serve most purposes,
but you can also install it from the sources, and then you can try some of Bertot's extensions.


The version of Isabelle used will be Isabelle 2004.
The user-interface for Isabelle will be Proof General run in XEmacs.

Other systems

The following systems will also be discussed, but as far as we know now they will not be part of the practical sessions:

Pre-installed software

As additional help for installing the software we provide the installation log from an IBM T40 1500MHz laptop running RedHat Enterprise Linux, kernel 2.6. See the following file: install.log .

Resource directory

Here is a directory with the various resource files mentioned in the above text. We might add things here later. Feel free to browse: resources/

[To TYPES School Main Page]
Last modified: Wed Jun 29 15:00:39 MEST 2005, by David Wahlstedt