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).^[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]

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.

[1]

[2]

[3]