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

Systems

To download the systems presented in the course, together with their 2 dedicated interfaces.
  • Alfa.
    Contact: catarina@cs.chalmers.se.
  • Coq.
    Contact: Benjamin.Werner@inria.fr.
  • Isabelle.
    You only need to install HOL and HOL-Real. Please make sure that it works under Proof General.
    Contact: nipkow@in.tum.de.
  • PCoq.
    A user-interface for Coq.
    Contact: Yves.Bertot@sophia.inria.fr.
  • PhoX.
    Contact: raffalli@univ-savoie.fr.
  • Plastic.
    Contact: P.C.Callaghan@durham.ac.uk.
  • Proof General.
    An Emacs user-interface for Coq, Lego and Isabelle.
    Contact: David.Aspinall@dcs.ed.ac.uk.
  • Twelf.
    Contact: carsten@cs.yale.edu.
    • Francis Montagnac