Search
Menu
Home
Sources
About
Contacts
LEGO (proof assistant)
LEGO
is a
proof assistant
developed by
Randy Pollack
at the
University of Edinburgh
. It
implements
several
type
theories: the
Edinburgh Logical Framework
, the
Calculus of Constructions
, the
Generalized Calculus of Constructions
and the
Unified Theory of Dependent Types
.