Types summer school'99: Theory and practice of formal proofs

Giens, France, August 30 - September 10, 1999

Systems

To download the 4 systems to be used in the course, together with their 2 dedicated interfaces:
  • Alfa
    Contact: hallgren@cs.chalmers.se, catarina@cs.chalmers.se
  • Coq
    In order to be able to use CtCoq (see below), you should download the previous version of Coq: 6.2.4.
    The last version (6.3) will not be available at the school.
    Contact: Benjamin.Werner@inria.fr.
  • CtCoq
    A Centaur interface for Coq. Needs the previous version of Coq: 6.2.4.
    Contact: Yves.Bertot@sophia.inria.fr
  • Isabelle
    You should install the RPM packages smlnj-110, isabelle, and isa-HOL. Note that the standard Isabelle distribution is already included, with all sources.
    Contact: Tobias.Nipkow@informatik.tu-muenchen.de
  • Lego
    For easiest installation, we recommend Red Hed Linux. To use Lego effectively, you should provide the Proof General Emacs interface, too.
    Contact: Zhaohui.Luo@durham.ac.uk
  • Proof General
    An Emacs interface for Coq, Lego and Isabelle.
    Contact: David.Aspinall@dcs.ed.ac.uk
    • Joelle.Despeyroux@inria.fr