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.