Implementations Emerging from the TYPES BRA
- 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.
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