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

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

References

↑ "Software Search - zbMATH Open". zbmath.org. Retrieved 2022-11-03.
↑ McBride, Conor (2006). "Lego". In Wiedijk, Freek (ed.). The Seventeen Provers of the World. Lecture Notes in Computer Science. Vol. 3600. Springer. pp. 118–126. ISBN 978-3-540-30704-4.
↑ Barendregt, Henk; Geuvers, Herman (2001). "Proof-assistants using dependent type systems". Handbook of Automated Reasoning. Vol. 2. Elsevier and MIT Press. pp. 1149–1238.

External links

Official website

[1] "Software Search - zbMATH Open". zbmath.org. Retrieved 2022-11-03.

[2] McBride, Conor (2006). "Lego". In Wiedijk, Freek (ed.). The Seventeen Provers of the World. Lecture Notes in Computer Science. Vol. 3600. Springer. pp. 118–126. ISBN 978-3-540-30704-4.

[3] Barendregt, Henk; Geuvers, Herman (2001). "Proof-assistants using dependent type systems". Handbook of Automated Reasoning. Vol. 2. Elsevier and MIT Press. pp. 1149–1238.