LEGO es un asistente de pruebas desarrollado por Randy Pollack en la Universidad de Edimburgo . Implementa varias teorías de tipos: el Marco Lógico de Edimburgo (LF), el Cálculo de Construcciones (CoC), el Cálculo de Construcciones Generalizado (GCC) y la Teoría Unificada de Tipos Dependientes (UTT).