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

developed by Randy Pollack at the

University of Edinburgh The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 15 ...

. It implements several type theories: the

Edinburgh Logical Framework In logic, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework typ ...

(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 reason, ...

(CoC), the Generalized Calculus of Constructions (GCC) and the

Unified Theory of Dependent Types Unified may refer to: * The Unified, a wine symposium held in Sacramento, California, USA * ''Unified'', the official student newspaper of Canterbury Christ Church University * UNFD, an Australian record label * ''Unified'' (Sweet & Lynch album) ...

(UTT).

References

External links

* Proof assistants Dependently typed languages {{mathlogic-stub