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 (LF), the Calculus of Constructions (CoC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT).{{Cite web |title=Software Search - zbMATH Open |url=https://zbmath.org/software/9685 |access-date=2022-11-03 |website=zbmath.org}}