LEGO is a programming language created in 1992 by Randy Pollack.
| #1771on PLDB | 33Years Old |
LEGO is an interactive proof assistant developed by Randy Pollack at the University of Edinburgh. It implements type theories including the Edinburgh Logical Framework (LF), Calculus of Constructions (CoC), Generalized Calculus of Constructions (GCC), and Unified Theory of Dependent Types (UTT), supporting formal proof development in natural deduction style.