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.
• 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.