LEGO is a

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof edi ...

developed by Randy Pollack at the

University of Edinburgh The University of Edinburgh (, ; abbreviated as ''Edin.'' in Post-nominal letters, post-nominals) is a Public university, public research university based in Edinburgh, Scotland. Founded by the City of Edinburgh Council, town council under th ...

. It implements several type theories: the Edinburgh Logical Framework (LF), the

Calculus of Constructions In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reaso ...

(CoC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT).

References

External links

* Proof assistants Dependently typed languages {{Mathlogic-stub