LEGO (proof assistant)
Proof assistant
From Wikipedia, the free encyclopedia
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).[1]
LEGO is described together with another sixteen interactive theorem provers, in a dedicated chapter written by Conor McBride in Freek Wiedijk's comparative study The Seventeen Provers of the World.[2] Henk Barendregt and Herman Geuvers also discuss LEGO in their survey chapter on proof assistants, grouping it with Coq and Agda as systems built on the same logic.[3]