- LEGO - an interactive proof assistant for an extension of the Calculus of Constructions, developed at Edinburgh.
- Coq - an interactive proof assistant for the Inductive Calculus of Constructions.
- Ctcoq - A graphical interface for Coq using Centaur.
- ALF.
- Isabelle is a generic theorem prover. New logics are introduced by specifying their syntax and rules of inference. Proof procedures can be expressed using tactics and tacticals.

Return to TYPES homepage

Last updated on 11 March 1996 by Healfdene Goguen <hhg@dcs.ed.ac.uk>